4 ms·

"I believe that no human, alive or dead, knows all the details of the proof of Fermat’s Last Theorem. But the community accept the proof nonetheless," Buzzard w

by Ceezy 7y ago

"I believe that no human, alive or dead, knows all the details of the proof of Fermat’s Last Theorem. But the community accept the proof nonetheless," Buzzard wrote in a slide presentation[...] That s 100% clickbait. People knows the demonstration and the demonstration helped to create entire new fields. By the way there are new and shorter proof of the theorem.

hyperbovine 7y ago
Also, that is quite a remarkable and provocative statement given that Andrew Wiles is still very much alive.
- foooobar 7y ago
  Buzzard asked Wiles himself, who stated "that he would not want to sit an exam on the proof of Langlands–Tunnell".
- repolfx 7y ago
  I think the intended implication is that Wiles has not read or understood all of the proofs he built on. If someone said, "nobody dead or alive understands all the details of Windows" I doubt anyone here would find it controversial. It's too big to fit in one person's head.
- Stasis5001 7y ago
  Sure, Wiles obviously understands the main thrust of his proof. But one could argue that Wiles' result depends on lots of other results, which in turn depend on other results, and so on through decades and decades of work, ultimately going back to the foundations of mathematics. Neither Wiles nor anybody else can claim to rigorously understand all of it. You can imagine this as a tree, with Wiles' work as root, and his dependencies as ancestors, and so on. An error at a lower level of the tree could, in theory, invalidate the root node. I do agree with Buzzard that it's hard to be sure. I've definitely read papers where a critical argument isn't well written or what is written seems wrong. However, if there are low-level errors, I suspect that with some work things could be patched up.
  - hyperbovine 7y ago
    Right, speaking as a lapsed mathematician, I definitely see errors or gaps in published work. Wiles’ original FLT proof had one. And yes these can generally be patched up. I’m not quite as alarmed as the author is, because generally a major false result would have all sorts of alarming ripple effects and implications which would be pretty easy to spot. FLT is an extreme example where literally anyone with a calculator could in theory disprove it. The fact that no one has suggests to me that it’s likely true.
  - Ceezy 7y ago
    You don t need to understand everything. People spend there all lives creating new demonstrations. Each one is a new prospective on a subject. And if the first one was made of milions of nodes an other one can be made of two nodes only. Take the index theorem there are proofs that have nothing to do with each othere some are very long some aren t. And finally from the beginning of math people misunderstand their on theorems, doesn t mean that there students won t do better.
robinhouston 7y ago
There’s a great discussion of this on Buzzard’s blog. https://xenaproject.wordpress.com/2019/09/27/does-anyone-know-a-proof-of-fermats-last-theorem/ https://xenaproject.wordpress.com/2019/09/27/does-anyone-kno... Read the comments too.
- deleted 7y ago
  [deleted]
- YeGoblynQueenne 7y ago
  One of the commenters wonders why we can trust a proof assistant more than a human: >> if one needs a program to check all the proofs, who’s gonna check that program? Another program-checking program? And a program-checking-program-checking program, etc.? To which Buzzard's reply is that, well, computer scientists have done a thorough job proving the correctness of proof assistants: >> To check that Lean has correctly verified a proof, we don’t need to check that Lean has no bugs, we just need to check that it did its job correctly on that one occasion, and this is what the typecheckers can do. This is a technical issue and you’d be better off talking to a computer scientist about this, but they have thought about this extremely carefully. Reading this as a computer scientist whose field of study is buiilt on automated theorm proving and logic programming (not what proof assistants do, exactly, but close, and some proof assistants even use resolution theorem proving, I understand) this is placing way too much trust on computer scientists. Every bit of theory on automated theorem proving that has ever been published is like maths: theorems are proved by hand, on paper, by humans. And some proofs can be quite convoluted. There's nothing approaching the complexity of the mathematical proofs that make Kevin Buzzard worry, but still, the proofs are not trivial and there is plenty of scope for error. So I'm afraid that even with computer-aided proofs, we 're still building castles on sand. Which is quite shocking if you think about it. We think that, maybe we can't trust our minds to know anything with any certainty, but we can trust computers to be flawless in their computations. But how do we know that with any certainty, if we can't know anything with any certainty?
  - digama0 7y ago
    Luckily, this is a solvable problem. A theorem prover is software, so you can apply formal methods to it, and prove that the software performs its stated function. The CakeML project does this, and I'm working on a bootstrapping theorem prover (Metamath Zero) to do this in a few hundred lines of code. So it's not as hopeless as it seems. You just have to have a really efficient and simple checking algorithm and run it over a big computer generated proof of correctness, and it all scales very well. Then you can take that verified theorem prover and apply it to all the regular math we care about.
deleted 7y ago
[deleted]

by Ceezy 7y ago

hyperbovine 7y ago

Also, that is quite a remarkable and provocative statement given that Andrew Wiles is still very much alive.

foooobar 7y ago
Buzzard asked Wiles himself, who stated "that he would not want to sit an exam on the proof of Langlands–Tunnell".
repolfx 7y ago
I think the intended implication is that Wiles has not read or understood all of the proofs he built on. If someone said, "nobody dead or alive understands all the details of Windows" I doubt anyone here would find it controversial. It's too big to fit in one person's head.
Stasis5001 7y ago
Sure, Wiles obviously understands the main thrust of his proof. But one could argue that Wiles' result depends on lots of other results, which in turn depend on other results, and so on through decades and decades of work, ultimately going back to the foundations of mathematics. Neither Wiles nor anybody else can claim to rigorously understand all of it. You can imagine this as a tree, with Wiles' work as root, and his dependencies as ancestors, and so on. An error at a lower level of the tree could, in theory, invalidate the root node. I do agree with Buzzard that it's hard to be sure. I've definitely read papers where a critical argument isn't well written or what is written seems wrong. However, if there are low-level errors, I suspect that with some work things could be patched up.
- hyperbovine 7y ago
  Right, speaking as a lapsed mathematician, I definitely see errors or gaps in published work. Wiles’ original FLT proof had one. And yes these can generally be patched up. I’m not quite as alarmed as the author is, because generally a major false result would have all sorts of alarming ripple effects and implications which would be pretty easy to spot. FLT is an extreme example where literally anyone with a calculator could in theory disprove it. The fact that no one has suggests to me that it’s likely true.
- Ceezy 7y ago
  You don t need to understand everything. People spend there all lives creating new demonstrations. Each one is a new prospective on a subject. And if the first one was made of milions of nodes an other one can be made of two nodes only. Take the index theorem there are proofs that have nothing to do with each othere some are very long some aren t. And finally from the beginning of math people misunderstand their on theorems, doesn t mean that there students won t do better.

robinhouston 7y ago

There’s a great discussion of this on Buzzard’s blog. https://xenaproject.wordpress.com/2019/09/27/does-anyone-know-a-proof-of-fermats-last-theorem/ https://xenaproject.wordpress.com/2019/09/27/does-anyone-kno... Read the comments too.

deleted 7y ago
[deleted]
YeGoblynQueenne 7y ago
One of the commenters wonders why we can trust a proof assistant more than a human: >> if one needs a program to check all the proofs, who’s gonna check that program? Another program-checking program? And a program-checking-program-checking program, etc.? To which Buzzard's reply is that, well, computer scientists have done a thorough job proving the correctness of proof assistants: >> To check that Lean has correctly verified a proof, we don’t need to check that Lean has no bugs, we just need to check that it did its job correctly on that one occasion, and this is what the typecheckers can do. This is a technical issue and you’d be better off talking to a computer scientist about this, but they have thought about this extremely carefully. Reading this as a computer scientist whose field of study is buiilt on automated theorm proving and logic programming (not what proof assistants do, exactly, but close, and some proof assistants even use resolution theorem proving, I understand) this is placing way too much trust on computer scientists. Every bit of theory on automated theorem proving that has ever been published is like maths: theorems are proved by hand, on paper, by humans. And some proofs can be quite convoluted. There's nothing approaching the complexity of the mathematical proofs that make Kevin Buzzard worry, but still, the proofs are not trivial and there is plenty of scope for error. So I'm afraid that even with computer-aided proofs, we 're still building castles on sand. Which is quite shocking if you think about it. We think that, maybe we can't trust our minds to know anything with any certainty, but we can trust computers to be flawless in their computations. But how do we know that with any certainty, if we can't know anything with any certainty?
- digama0 7y ago
  Luckily, this is a solvable problem. A theorem prover is software, so you can apply formal methods to it, and prove that the software performs its stated function. The CakeML project does this, and I'm working on a bootstrapping theorem prover (Metamath Zero) to do this in a few hundred lines of code. So it's not as hopeless as it seems. You just have to have a really efficient and simple checking algorithm and run it over a big computer generated proof of correctness, and it all scales very well. Then you can take that verified theorem prover and apply it to all the regular math we care about.

deleted 7y ago

[deleted]