alt Hacker News> checking an existing fully fleshed out proof is simple
The controversy around Mochizuki and the "abc Conjecture" proof is a contrary example.
Replies
How does this involve computer checking of a formal proof?
Last time I checked, it was a disagreement over whether an informal proof is sound, which is exactly the problem with informal proofs.
ETA: There might be a misunderstanding about what "formal proof" means. Even a very detailed, precise English-language description of a proof is generally not a formal proof. The bar is essentially: "It could be checked by a machine that follows simple rules." If different interpretations of a "proof" are possible, the "proof" is by definition informal. Informal proofs are valuable because they are strong evidence that there's a corresponding formal proof "underneath" that would establish the theorem's truth, and because they are (usually) much easier to understand.
His partisans are trying to formalize his proof. I expect they're not going to be able to do it, because the proof is flawed.
This is one of the great things about formalization: it would have avoided this entire debacle.