Comment by jibal

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.