[FOM] formal proofs (was: Hersh on Flyspeck

[Hendrik Boom]

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.

-- hendrik