[FOM] formal proofs (was: Hersh on Flyspeck
hendrik at topoi.pooq.com
Sat Oct 11 22:34:04 EDT 2014
When a proof of a major theorem has been completely formalized and
mechanically checked there is a tendency to think, "So what? It was a
lot of work, but we already knew the theorem was true."
Perhaps machine proof-checking will finally come of age when an attempt
to check an important proof reveals that the informal version of
the proof is critically flawed in a way that isn't a mere lack of
formality, and places the truth of the theorem in doubt.
More information about the FOM