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

81–90 of 275 posts

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

#81

Post by wtallis »

mrob wrote: post #57
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…

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.

I participated in a discussion on /r/math about this a few months ago, and there was surprising resistance to ideas like this. Most of it fell into two categories. The first was people with a paper fetish who refuse to believe that there are now computer display technologies that provide adequate readability and resolution to be a full-time substitute for books. The second was people who can't imagine a usable way to typeset proofs that embed metadata about which lines are the key steps and which could be folded. This is probably influenced by the fact that LaTeX doesn't support this kind of semantic markup and it would be awkward to add.

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

#82

Post by danharaj »

mrob wrote: post #57
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…

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.

Why can they? You can't assume fully explicit proofs are practical just because they're plausible. The justification of practicality will be highly nontrivial. If its impractical to write such a textbook then code folding gets you nothing.

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

#83

Post by dan-robertson »

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…

There’s this curious thing in mathematics where most things are either obviously true or obviously false and those that aren’t are mostly inconsequential. Those that remain are certainly more interesting but also typically their proofs are a few obvious steps.

Obvious in this case means something like “clear to a mathematician familiar with the field” or “otherwise many things will fall apart”

This leads to the situation where if a mistake is found in a theorem then it is likely still true even if the proof is wrong.

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

#84

Post by mrob »

danharaj wrote: post #82
mrob wrote: post #57

Earlier quoted context omitted.

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.

Why can they? You can't assume fully explicit proofs are practical just because they're plausible. The justification of practicality will be highly nontrivial. If its impractical to write such a textbook then code folding gets you nothing.

If it is impractical now, that simply means the software needs improvement. If mathematicians stop being so accepting of informal proofs then there is a very strong incentive to improve the software.

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

#85

Post by [deleted] »

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…

[deleted]

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

#86

Post by FabHK »

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…

> Mathematics textbooks would be intractably longer if they spelled out every step in explicit, formal detail.

Just as an example, Russell & Whitehead's Principia Mathematica famously requires some 400+ pages to prove that 1+1=2 (well, they prove some other stuff, too, I suppose.)

See the image and caption here to get a flavour: https://en.wikipedia.org/wiki/Principia_Mathematica

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

#87

Post by pmiller2 »

barbecue_sauce wrote: post #64
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…

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

Trust me, an MS in math doesn't even get you to the fun part. :)

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

#88

Post by kstrauser »

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…

I think you're exactly right. Mochizuki's work may or may not turn out to be sound, but in the mean time he's failed to communicate it to other experts, even when they've met with him in person for the specific goal of understanding his reasoning.

It's not sufficient to have a great idea, or even to be right about it. You have to be able to explain it thoroughly enough that other qualified peers can understand your logic enough to weigh in on it. That seems not to have happened yet hear.

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

#89

Post by yesenadam »

wtallis wrote: post #81
mrob wrote: post #57

Earlier quoted context omitted.

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.

I participated in a discussion on /r/math about this a few months ago, and there was surprising resistance to ideas like this. Most of it fell into two categories. The first was people with a paper fetish who refuse to believe that there are now computer display technologies that provide adequate readability and resolution to be a full-time substitute for books. The second was people who can't imagine a usable way to…

people with a paper fetish who refuse to believe

Maybe there was surprising resistance because you spoke like that?

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

#90

Post by konschubert »

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…

I just have a Master in Physics, but here is my take:

The thing is that mathematic proofs work on different levels of "zoom", ranging from just stating "it follows trivially" to formal proofs. And this is a normal process, that's how Mathematicians boil down long proofs to simple lines of reasoning.

I think what happens here I that the author of the original proof is arguing on a high "it's obvious" level and seems to be unwilling to go into detail.

Post reply on HN