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

131–140 of 275 posts

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

#131

Post by smadge »

atmanthedog wrote: post #93
ericsoderstrom wrote: post #40

Earlier quoted context omitted.

Math is different in that one feels there should be something close to "absolute truth." That is, given a set of axioms, it is possible to verify with complete certainty whether a proof follows from those axioms or not. Though when proofs become so long and abstruse that only a handful of people can even read them, perhaps that's no longer true. In other fields, it's more clear that nothing is known with 100% certain…

Unfortunately, math doesn't really permit this type of truth: if your axioms are strong enough to prove general statements about arithmetic, there is no effective procedure to determine whether an arbitrary proof follows from those axioms.

Did you mean to write “there is no effective procedure to determine whether an arbitrary formula follows from those axioms?”

A proof is exactly how we demonstrate that a formula follows from the axioms.

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

#132

Post by nixpulvis »

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…

Who proves that the automated proof is correct. Who proves that... etc.

All this is tied up in Gödel's incompleteness theorem.

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

#133

Post by dwheeler »

nixpulvis wrote: post #132
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…

Who proves that the automated proof is correct. Who proves that... etc. All this is tied up in Gödel's incompleteness theorem.

Verifying proofs is a much simpler job than creating a proof. Also, you can have multiple independently implemented verifiers, which act in many ways like multiple human reviewers. That is what the metamath community does, they have 4 independently implemented verifiers that check every proof. That is very strong evidence that a proof is correct, far stronger evidence than is typically accepted now.

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

#134

Post by dwheeler »

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.

There are number of proof verification systems that do not require constructive logic. So if you require classical logic, just use a tool that supports it.

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

#135

Post by Sniffnoy »

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…

This is where Terry Tao's comment from December seems relevant: https://galoisrepresentations.wordpress.com/2017/12/17/the-a...

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

#136

Post by dwheeler »

nixpulvis wrote: post #132
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…

Who proves that the automated proof is correct. Who proves that... etc. All this is tied up in Gödel's incompleteness theorem.

Gödel's incompleteness theorem shows the inherent limitations of every formal axiomatic system capable of modelling basic arithmetic. The incompleteness theorem does not show that nothing can be proven.

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

#137

Post by nixpulvis »

dwheeler wrote: post #136
nixpulvis wrote: post #132

Earlier quoted context omitted.

Who proves that the automated proof is correct. Who proves that... etc. All this is tied up in Gödel's incompleteness theorem.

Gödel's incompleteness theorem shows the inherent limitations of every formal axiomatic system capable of modelling basic arithmetic. The incompleteness theorem does not show that nothing can be proven.

Who said anything about nothing ;)

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

#138

Post by MauranKilom »

MaxBarraclough wrote: post #72
cycrutchfield wrote: post #26

Earlier quoted context omitted.

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…

> 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?

I find his explanation of the reverse quite clear:

> Any proof that can be spelled out at a level of detail sufficient to be analyzed by a computer is necessarily going to consist entirely of steps that are each completely comprehensible to a mathematician.

This means there must either be a lot of steps or a lot of different paths to follow in order for a computer to be of use. Neither is the case here.

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

#139

Post by tandr »

Smaug123 wrote: post #98
barbecue_sauce wrote: post #64

Earlier quoted context omitted.

You have an MSc in mathematics but don't consider yourself an expert?

Where high-school mathematics was analogous to learning to form letters with a pencil, undergraduate BSc mathematics is analogous to learning to form words and short sentences. By the end of your BSc in the analogy, you can look at a sentence and recognise at least what sort of genre it might be part of, and you can write down many of the most common words as well as a number of rehearsed useful sentences. An MSc is…

This is beautiful. Thank you.

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

#140

Post by stepvhen »

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…

Well, first, use a logic programming language and report back. Then understand that math is almost wholly non-empirical. The things discovered or made up in math are not reflective of the real world, most of the time, regardless of how closely it resembles.

Take for instance euclidean geometry. In the world of equations, everything works. But a point, or a line, are neither things that exist out in the world, much less their relations which, when drawn on the surface of the earth, are probably not actually euclidean at all.

Number theory in particular is almost never about math, but about the patters mathematicians believe they recognize. Somebody a'ong the lines goes "oh hey check out this flower. I bet this is the only flower of this type in the world" and then spend hundreds of years trying to prove it.

Post reply on HN