Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

quantamagazine.org

Post reply on HN
Print view View original

51–60 of 275 posts

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#51

Post by bollu »

vbezhenar wrote: post #42
salty_biscuits wrote: post #27

Earlier quoted context omitted.

The really interesting case here is Voevodsky, who found an error in one of his own proofs many years later and then got interested in foundations of Mathematics and automated proofs. Homotopy type theory is an interesting development, particularly if you are into programming languages.

I don't really understand why the entire known mathematics is not automatically proven yet. We, people, understand very formal proofs. Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. I'm not talking about computer prooving theorem himself, but mathematician should write proof using some formal language and computer should be able to follow that…

If you've ever tried encoding proofs in a proof assistant such as Coq (which is what the INRIA folks used to encode the four color theorem and the Fiet-Thompson theorem), you'll realise just how painful it is --- I speak as someone who's done this for fun (and now for research. [my report is available here](https://github.com/bollu/dependence-analysis-coq/blob/master...)

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#52

Post by nabla9 »

vbezhenar wrote: post #42
salty_biscuits wrote: post #27

Earlier quoted context omitted.

The really interesting case here is Voevodsky, who found an error in one of his own proofs many years later and then got interested in foundations of Mathematics and automated proofs. Homotopy type theory is an interesting development, particularly if you are into programming languages.

I don't really understand why the entire known mathematics is not automatically proven yet. We, people, understand very formal proofs. Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. I'm not talking about computer prooving theorem himself, but mathematician should write proof using some formal language and computer should be able to follow that…

Formal proof assistants and interactive theorem prover for mathematics already exist. So do proof libraries. See: http://metamath.org/

They are not used because it's tedious to type and proof every step in the process. Mathematicians don't write all steps down. You also need build a library from ground up.

We could to the same for computer programs but we don't wan to do that either.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#53

Post by jackfoxy »

Moodles wrote: post #12

I have a MSc in mathematics so I am by no means an expert in mathematics proofs but I get the gist of it. To me a proof is literally a logical argument that you can follow to "believe" that a theorem is true. I do worry how many people actually understand or verify mathematics proofs. How many people have actually read and verified Perelman's or Wiles' proofs (I'm only singling them out because they're famous, not be…

Wasn't this very issue what inspired Voevodsky to work on a Univalent foundations of mathematics, resulting in the HoTT Book (in collaboration with others)?

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#54

Post by nabla9 »

mehrdadn wrote: post #48
vbezhenar wrote: post #42

Earlier quoted context omitted.

I don't really understand why the entire known mathematics is not automatically proven yet. We, people, understand very formal proofs. Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. I'm not talking about computer prooving theorem himself, but mathematician should write proof using some formal language and computer should be able to follow that…

Edit: never mind, it seems I confused deriving a proof with verifying it!

vbezhenar is talking about verifying proofs not finding proofs.

Computers can easily verify that proof is correct once the proof is written down using formal semantics. Proof checkers already exist.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#55

Post by andrepd »

vbezhenar wrote: post #42
salty_biscuits wrote: post #27

Earlier quoted context omitted.

The really interesting case here is Voevodsky, who found an error in one of his own proofs many years later and then got interested in foundations of Mathematics and automated proofs. Homotopy type theory is an interesting development, particularly if you are into programming languages.

I don't really understand why the entire known mathematics is not automatically proven yet. We, people, understand very formal proofs. Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. I'm not talking about computer prooving theorem himself, but mathematician should write proof using some formal language and computer should be able to follow that…

You don't understand because you haven't looked into it very much :) You'll find that automated theorem proving and proof verification is far from trivial. State of the art tools are still very cumbersome and verbose to use and are infeasible to use in those problems where you need them the most.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#56

Post by noisem4ker »

bollu wrote: post #51
vbezhenar wrote: post #42

Earlier quoted context omitted.

I don't really understand why the entire known mathematics is not automatically proven yet. We, people, understand very formal proofs. Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. I'm not talking about computer prooving theorem himself, but mathematician should write proof using some formal language and computer should be able to follow that…

If you've ever tried encoding proofs in a proof assistant such as Coq (which is what the INRIA folks used to encode the four color theorem and the Fiet-Thompson theorem), you'll realise just how painful it is --- I speak as someone who's done this for fun (and now for research. [my report is available here]( https://github.com/bollu/dependence-analysis-coq/blob/master... )

https://github.com/bollu/dependence-analysis-coq/blob/master...

Put a space before the final ), else it becomes part of the URL. Thanks for the paper, by the way.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#57

Post by mrob »

danharaj wrote: post #50
vbezhenar wrote: post #42

Earlier quoted context omitted.

I don't really understand why the entire known mathematics is not automatically proven yet. We, people, understand very formal proofs. Mathematics is very strict science with axioms and following theorems. It should be a perfect application for computing. I'm not talking about computer prooving theorem himself, but mathematician should write proof using some formal language and computer should be able to follow that…

> Mathematics is very strict science with axioms and following theorems. Mathematics textbooks would be intractably longer if they spelled out every step in explicit, formal detail. And then the proofs wouldn't make sense to people because the core ideas would be obscured by the formality! A typical mathematics proof is intended to be read by a thinking human assumed to have some level of mathematical sophistication…

Why can't textbooks use code-folding style display to hide unwanted detail? Paper books are basically obsolete except as a master copy for archival.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#58

Post by trevyn »

cycrutchfield wrote: post #26
peq wrote: post #21

Mathematicians should do more computer verifiable proofs to avoid discussions like this. > Definitions went on for pages, followed by theorems whose statements were similarly long, but whose proofs only said, essentially, “this follows immediately from the definitions.” This sounds perfect for machine checked proofs, but I guess the proofs are actually a lot more involved than they are presented.

Per Peter Scholze (from https://galoisrepresentations.wordpress.com/2017/12/17/the-a... ): >One final point: I get very annoyed by all references to computer-verification (that came up not on this blog, but elsewhere on the internet in discussions of Mochizuki’s work). The computer will not be able to make sense of this step either. The comparison to the Kepler conjecture, say, is entirely misguided: In that case, th…

Well that's sort of the point, isn't it? If you can't make the computer make sense of it, you have no proof.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#59

Post by dagw »

xxpor wrote: post #4
drenvuk wrote: post #2

I think this would count as esoteric if you ignore the drama portion of it. Just to get to the point of understanding what they're talking about would probably take months of dedicated uninterrupted work. Neat. I have no idea where to even start. https://en.wikipedia.org/wiki/Anabelian_geometry

I think what makes these number theory arguments so interesting to me is how simple the theorems are, but how impenetrable the proofs are. For example, Fermat's last theorem is so easy to understand, but there's no chance in hell I'll ever understand Wiles' paper proving it.

You might not understand all the details of the paper, but you can definitely follow the thrust of the argument and see the elegance in it without advanced math skills.

The really hard part (and main part of Wile's contribution to the proof) was proving something called the Taniyama–Shimura–Weil conjecture. However if you skip that bit and just accept that the conjecture is true the rest of the steps of the proof are both elegant and relatively easy to follow (if you gloss over some of the details) for anybody with a decent grasp of basic math.

The book Fermat's Last Theorem by Simon Singh is a pretty great read and does a good job of outlining the basic structure of the proof for anybody with a decent grasp of high school mat.

Re: Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

#60

Post by westoncb »

> “The abc conjecture is a very elementary statement about multiplication and addition,” said Minhyong Kim of the University of Oxford. It’s the kind of statement, he said, where “you feel like you’re revealing some kind of very fundamental structure about number systems in general that you hadn’t seen before.”

I can kind of see that, but there's something in it that gives me the feeling of arbitrariness.

It's looking at the relationship between prime factors of A, B, C in A + B = C, where no prime factors may be shared between A, B, or C. The specific relationship in question is between the magnitude of C and the unique prime factors of A, B, and C multiplied together.

To take an example from the article, 5 + 16 = 21 meets the basic requirements since the prime decomposition looks like (5) + (2 * 2 * 2 * 2) = (7 * 3) —no factors are shared. But, the quantity we're supposed to relate to C is (5 * 2 * 7 * 3), since it is the product only of the unique primes.

Does that not feel arbitrary, to drop the repetitions? So it ends up being that the sought out smaller products arise because they had large numbers of repetitions, so we removed more when forming the product.

But I suppose there are probably just some deep number theory mysteries behind it which give justification, so it only feels arbitrary to someone like myself who is basically ignorant on the subject :)

Post reply on HN