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.

▲

monkeyelite 5 days ago | parent | next [-]

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,

	▲	okintheory 5 days ago \| parent [-]
		You're wrong. The mistake could have been unfixable. That happens quite frequently (see: countless retracted claimed proofs of major results by professional mathematicians).

▲

monkeyelite 5 days ago | parent | prev [-]

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

▲

robinzfc 4 days ago | parent [-]

The purpose of math is indeed to increase our understanding, but the correctness of proofs is a precondition for that. A wrong proof does not increase understanding, although it may create such illusion. Proof assistants provide scalability to correctness checking and this way they contribute to understanding.

Some proof assistants contribute more directly to understanding by making proofs easier to study.

	▲	jibal 3 days ago \| parent [-]
		Indeed. Strange that the previous commenter attacked such an obvious strawman ... they responded to my statement about the purpose of proof with a statement about the purpose of math, which I hadn't mentioned. Also strange is the claim that the purpose of a proof is to show "why" a statement is true rather than that a statement is true. Some proofs help understand the "why" but many don't (proofs of the FLT included) and informal discussion is usually better for that, and is often why we believe that an unproven proposition is true -- e.g., it's widely believed, for good reasons, that P != NP, but no one knows how to prove it. Ditto for the Collatz conjecture.