11 ms·

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://xe

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.
  - YeGoblynQueenne 7y ago
    But formal methods are also supported by theory where any theorems have proofs done by humans, which may contain mistakes. It's humans all the way down, see.

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.
- YeGoblynQueenne 7y ago
  But formal methods are also supported by theory where any theorems have proofs done by humans, which may contain mistakes. It's humans all the way down, see.