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

71–80 of 275 posts

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

#71

Post by naasking »

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…

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

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

#72

Post by MaxBarraclough »

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…

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

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

#74

Post by auggierose »

A few years ago I asked Mochizuki via email if he would be interested in organising with me an effort to mechanise his proof. At the time I was developing a collaborative interactive theorem prover, for which this would be an ideal application. He politely declined, and I am kind of happy about this now, because I need a few more years anyway before my theorem prover could be used for something like this without being a pain for its users :-D

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

#75

Post by dan-robertson »

CodeSheikh wrote: post #70

My God! This Titans' website needs urgent attention: http://www.kurims.kyoto-u.ac.jp/~motizuki/top-english.html

Why? It might be worse than a

and a with links to papers but it loads ok and it’s basically a point of pride amongst academics to have an ancient or amateurish looking handmade website. Perhaps it is a signal that time is spent on academic work or a that the site was made by the academic (and so has useful materials for academics) and not by some publicist who does not provide useful academic materials.

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

#76

Post by westoncb »

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 entirely new, super general system. But you can imagine if Grothendieck for example had done all of his work for years and years in isolation and then presented Schemes, Topoi, and Motives to everyone all at once, using them in combination to prove something familiar, and expecting other mathematicians to just learn and understand them all in order to verify a single proof.

I think in that case, folks would not have been immediately so interested in the new constructions Grothendieck had come up, viewing it initially as mountains of unnecessarily alien concepts built up just to give other mathematicians a hard time ;)

(Not to identify the two mathematicians overly—I'm not sure how appropriate that really is—but I remember that being my impression when first digging into Mochizuki's work, and I haven't seen it mentioned here yet.)

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

#77

Post by zbobet2012 »

zbobet2012 wrote: post #67
danharaj wrote: post #50

Earlier quoted context omitted.

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

This is a common objection from mathematicians, that is very understandable. I think both Lamport and Voevodsky’s have made important contributions here [1]. Namely in presenting idea from software that we use to manage _exactly_ your complaint. The way in which mathematicians structure proofs has fallen behind the ways in which software engineers structure programs (which are isomorphic to proofs). The question is t…

It's also important to note that this situation is _precisely_ what Voevodsky wanted to prevent:

For nearly a decade, Voevodsky has been advocating the virtues of computer proof assistants and developing univalent foundations in order to bring the languages of mathematics and computer programming closer together. As he sees it, the move to computer formalization is necessary because some branches of mathematics have become too abstract to be reliably checked by people.

“The world of mathematics is becoming very large, the complexity of mathematics is becoming very high, and there is a danger of an accumulation of mistakes,” Voevodsky said. Proofs rely on other proofs; if one contains a flaw, all others that rely on it will share the error. [1]

Most mathematicians still think of machine check for dealing with a large _number_ of cases; but Homotopy Type Theories goal is to manage abstract complexity not just size.

[1]https://www.quantamagazine.org/univalent-foundations-redefin...

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

#78

Post by Jach »

CodeSheikh wrote: post #70

My God! This Titans' website needs urgent attention: http://www.kurims.kyoto-u.ac.jp/~motizuki/top-english.html

Why? At least it's not hot pink or otherwise eye-blinding. I still find it charming that many Japanese sites seem stuck in 90s web design. But recently I've been running into more Japanese sites that seem to have advanced to mid-2000s web design, with proper CSS and designs that use curves and angles and don't force everything into a box shape (visible or invisible)! That's my favorite era so I hope it's a while before they join the rest of us in bloated SPA hell.

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

#79

Post by danharaj »

zbobet2012 wrote: post #67
danharaj wrote: post #50

Earlier quoted context omitted.

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

This is a common objection from mathematicians, that is very understandable. I think both Lamport and Voevodsky’s have made important contributions here [1]. Namely in presenting idea from software that we use to manage _exactly_ your complaint. The way in which mathematicians structure proofs has fallen behind the ways in which software engineers structure programs (which are isomorphic to proofs). The question is t…

I own a copy of the HoTT book :)

> Namely the way in which mathematicians structure proofs has fallen behind the ways in which software engineers structure programs (which are isomorphic to proofs).

The problem is that the required structure for writing sophisticated mathematical proofs is much more demanding than even a piece of software as complex as the Linux kernel. Part of that is because software as such, when interpreted as proofs, don't verify properties nearly as strong as a real theorem. The difference between a proof of `Integer -> Integer` and `Integer -> Odd Integer` is already a gulf the vast majority of software does not bridge.

We're just not there yet. Voevodsky's program is a great first step but just that: A first step. No one really knows what the next thousand steps will be. It's not straightforward at all.

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

#80

Post by Angostura »

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…

Wouldn;t it bump into the same kind of problems that Bertrand Russell's attempts bumped into with the Principia Mathematica? Namely it crashed into Gödel's incomplete theorem?

Disclaimer: What I don't know bout maths would fill volumes, in both senses of the word

Edit: From the down-votes, apparently not.

Post reply on HN