Comment by kobebrookskC3
3 days ago
the proof is so complicated it's hard to trust if it's only on paper. if we formalize it, it can be checked by a computer.
3 days ago
the proof is so complicated it's hard to trust if it's only on paper. if we formalize it, it can be checked by a computer.
y/n of strict logical checking the least interesting part of a proof. It's the insight into why it's true or false that's valuable, and that insight of Wiles was enough to convince the rest of the math community.
In other words, the chance that we find gaps and mistakes in the written proof? 100% - the chance we find out it's false due to sloppy logic? 0%.
Wiles' original proof was flawed. It wasn't due to "sloppy logic", it was a subtle misapplication of a theorem when the conditions for its use weren't met. It wasn't merely a mistake or gap in the exposition ... the error required finding a different approach and it took Wiles and Taylor a year to patch the proof.
There are multiple reasons for formalizing the proof in Lean ... see https://github.com/ImperialCollegeLondon/FLT/blob/main/GENER...
P.S. "So that patching is exactly what I’m referring to."
No, it isn't.
"The mathematicians can see the idea that’s true"
Mathematicians could not "see" that FLT was true, and they could not "see" that Wiles' original proof demonstrated it because it didn't. His original flawed proof showed how certain tools could be used, but it didn't establish the truth of FLT. There long had been speculation that it was undecidable, and it might still have been until Wiles and Taylor provided a correct proof.
From a previous comment by the same user: "The purpose of a proof is to show yourself and someone else why something is true."
The purpose of a proof of an assertion is to demonstrate that the assertion is true. Once that is done, the assertion can be treated as a theorem and other results can be built upon it.
The purpose for digitally formalizing a proof of a theorem that has already been accepted as proven by the mathematical community is multifold, as laid out at the link above.
So that patching is exactly what I’m referring to. The mathematicians can see the idea that’s true, they just need to re-engineer it. That’s why they could move forward with confidence on an unsolved problem.
Lean helps with none of that. It doesn’t help you find proof ideas and it doesn’t help you communicate them,
1 reply →
> The purpose of a proof of an assertion is to demonstrate that the assertion is true. Once that is done, the assertion can be treated as a theorem and other results can be built upon it.
No. The purpose of math is to increase our understanding, not check off boxes.
In your model you might as well have a computer brute force generate logical statements and study those. Why would that be less valuable then an understanding of differential equations?
2 replies →
The specific example of Fermat's Last Theorem is probably true simply because so much work has been done on the modularity of elliptic curves since then, but the probability of false results being proven is much higher than 0%.
In fact, Buzzard has an "existence theorem" of this exact thing. Annals of Mathematics (one of the top mathematics journals) has published one paper proving a theorem, and another paper proving the opposite result of a theorem: https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/sli...
My claim is not that nobody ever makes mistakes, it’s formalizing in a computer is extremely high cost for very little reward and doesn’t help the core process of finding proof ideas