[FOM] formal proofs /query

[Michael Lee Finney]

When I was working on an experimental formal system, I had manually
created and verified several hundred proofs of elementary results in
that system. I wrote a proof verifier, and in spite of several people
manually checking the proofs, the proof verifier found errors in a
half-dozen proofs. Most were trivial and easily fixed, but some
required a complete rework of the proof. This was a small system and
none of the proofs were really difficult. But it is impossible for
people to be always perfect in anything so I believe that, long term,
all proofs must be mechanically verified before they are accepted.

So, even if we haven't seen it yet in major systems and proofs, I can
easily believe that proof verifiers will eventually find significant
errors in major proofs.

Michael Lee Finney


> 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

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