[FOM] formal proofs /query
Palma at ukzn.ac.za
Sun Oct 12 03:23:55 EDT 2014
Since I have not followed proof checks, can anyone tell me whether the question posed (by Hendrik Boom) has a positive answer?
Are there cases in which the check in terms of syntax done by the machines revealed a real flaw in a proof, in the informal or intuitive style?
From: fom-bounces at cs.nyu.edu [mailto:fom-bounces at cs.nyu.edu] On Behalf Of Hendrik Boom
Sent: 12 October 2014 04:34
To: fom at cs.nyu.edu
Subject: [FOM] formal proofs (was: Hersh on Flyspeck
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.
FOM mailing list
FOM at cs.nyu.edu
More information about the FOM