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

221–230 of 275 posts

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

#221

Post by m00n »

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…

To take one of your examples that I happen to be familiar with: Wiles' proof of FLT. I can assure you that in the >20 years that this proof has been out, thousands of professors, postdocs and grad students have read and reread every line of the two Annals papers.

They have been the foundation of hundreds of Phd projects and the scientific merit and public fame to be gained by finding a gap in the argument is clear.

Actually I think breakthrough papers are least problematic when it comes to unverified claims in math.

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

#222

Post by m00n »

jedharris wrote: post #207
jamesrcole wrote: post #178

Earlier quoted context omitted.

The term "proof" seems to be a lot of the problem, because it implies something definitive.

Excellent point. What mathematicians write to each other are arguments not proofs. Machine checkable proofs are really proofs. This should not be embarrassing to mathematicians. It opens up potential for a lot of progress in several directions. Arguments can become better ways to communicate with humans. Proofs can be developed where needed to resolve questions about arguments. The relationships between arguments and…

What is the philosophical difference between an 'argument' that human minds following the laws of logic agree on "is correct" and a machine built by these minds flashing a "correct light"?

IMO the only advantage to be gained by introducing physical computers in the picture is lightning-fast book keeping.

Why would you trust an Intel CPU, a Samsung SSD and a linux fs driver running some verifying framework more than the human brains designing, writing and executing said framework?

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

#223

Post by bsder »

fjsolwmv wrote: post #146
bsder wrote: post #22

Earlier quoted context omitted.

> True, but even then, how large do you think the field is? And how many people verify these proofs? It only takes one to break it. And, for something so fundamental, it's a big deal if you are the one. This isn't physics, where you have to rule out all manner of confounding data before you can trust your conclusion.

The point you are missing that studying a proof can't proof it correct, only fail to disprove it.

That's incorrect.

For example, given the axioms of Euclidean geometry, I can prove that the sum of the angles of a triangle add up to 180 degrees.

That statement is true. Full stop.

Now the starting axioms may not be correct (the parallel postulate, for example, is not required to be true). However, given the starting axioms, proofs are true. Period.

In addition, there will be things in mathematics that you cannot prove--Godel's Incompleteness Theorem sits in this section.

And, science has the problem that a hypothesis can only be disproven.

Mathematics does not suffer from the same issue, though.

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

#224

Post by MaxBarraclough »

konschubert wrote: post #101
MaxBarraclough wrote: post #72

Earlier quoted context omitted.

> The computer will not be able to make sense of this step either. What does that mean, then? That a leap is being made that depends on the reader's fuzzy intuitions, rather than the established axioms? If that's the case, it's not a formal proof at all, no? Or am I way off here?

Maybe he says that the computer won't help understand the proof since the proof is missing a step. He may be saying the equivalent of "A computer won't help you to prove that 1+1=3“

> He may be saying the equivalent of "A computer won't help you to prove that 1+1=3“

But it can. You need to have the computer 'comprehend' the relevant axioms, of course.

If your 'proof' is in fact just arguing the case for new axioms, that isn't a proof at all, it's a misunderstanding of what 'axiom' means. (They're definitions, not profound universal truths.)

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

#225

Post by emileokada »

resters wrote: post #111
bollu wrote: post #51

Earlier quoted context omitted.

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... )

What is the painful part? The level of detail required for it to check?

A lot of proofs at masters level and beyond omit a lot of details because they can easily be checked, but would be tedious to write out explicitly. This means that a 1 page proof would probably actually correspond to 2-3 pages (or more!) if written out with all the details (e.g. with standard but tedious arguments fleshed out properly, and all cases delt with explicitly (rather than resorting to a 'and the other cases follow through similarly' remark)). When written in a proof assistant this would become even longer because natural language allows us to brush a lot details under the carpet because they are understood from context.

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

#226

Post by Kutta »

naasking wrote: post #71
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…

Because most mathematics is not constructive, and most automated theorem proving tools are based on constructive logic.

That's irrelevant, all mainstream proof assistants are compatible with classical logic.

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

#228

Post by emileokada »

westoncb wrote: post #76
lacker wrote: post #69

I remember an instructor explaining during the math olympiad training program: "A proof doesn't have to be in any particular format. A proof is an argument that can convince other mathematicians." At this point, it seems clear that we do not have a proof of the ABC conjecture. Perhaps someone will be able to improve this to make a real proof - after all, there were some errors in the first Wiles proof of Fermat's Las…

It's interesting that this article doesn't touch on this aspect of the situation at all, but when reading about Mochizuki's proof in the past it was presented as clear that proving the ABC conjecture was one application of a new general theory—not that all of Mochizuki's innovations are tied specifically to that problem. I was given to understand that his work was more like Grothendieck's, where he's developing this…

I believe the article explicitly steers away from this because nearly all the discourse on this proof has been precisely about this (c.f. remark Scholze that 'The whole discussion surrounding the proof had gotten “too sociological,”').

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

#229

Post by AstralStorm »

darkmighty wrote: post #128
WalterGR wrote: post #100

Earlier quoted context omitted.

If you've ever tried encoding proofs in a proof assistant such as Coq... you'll realise just how painful it is Is that a result of how painful the tool is to use? (And by “tool” I mean any such tool - coq or whatever.) What would need to be improved in the state-of-the-art of automated proof validation for the process to be less painful?

> What would need to be improved in the state-of-the-art of automated proof validation for the process to be less painful? I think there are two parts: 1) Improve the theorem proving languages syntax so it's more intuitive, and so there is a wealth of "libraries" to build upon so you don't have to go from the basic axioms (of arithmetic or the reals for example) any time you wanted to prove something. 2) Provide some…

Isabelle semi-automatic theorem prover tries to help with 2 if you use sledgehammer strategy and print out the simplified proof with isar_proofs argument, which you can more easily read and reintegrate into the main document if needed.

You can help its heuristics by providing it a set of potential proof facts explicitly.

The libraries available for it are already quite huge... sometimes in a few encodings as well. (valued, typed, functional etc.)

https://www.isa-afp.org/

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

#230

Post by Jweb_Guru »

forkerenok wrote: post #193
WalterGR wrote: post #100

Earlier quoted context omitted.

If you've ever tried encoding proofs in a proof assistant such as Coq... you'll realise just how painful it is Is that a result of how painful the tool is to use? (And by “tool” I mean any such tool - coq or whatever.) What would need to be improved in the state-of-the-art of automated proof validation for the process to be less painful?

The bottleneck is not the tool itself, but the theory it builds upon: Calculus of Constructs in Coq's case. CoC and other calculi oriented towards proofs have limitations. To better understand current challenges with provers I can recommend this episode of the Type Theory podcast with Dan Licata as a guest: http://typetheorypodcast.com/2015/01/episode-3-dan-licata-on... It's quite dense, but there are some bits that…

The vast majority of formal proofs don't run into any limitations with the CiC. They run into more practical limitations with the tooling and available libraries and tactics.
Post reply on HN