[FOM] formal proofs /query

[Adriano Palma]

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?
Thank you

Palma


-----Original Message-----
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.

-- hendrik
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom