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.
> checking an existing fully fleshed out proof is simple
The controversy around Mochizuki and the "abc Conjecture" proof is a contrary example.
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.