[FOM] formal proofs /query

[Timothy Y. Chow]

Adriano Palma wrote:
> 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

I'm pretty sure that the short answer is no, but the longer and more 
accurate answer IMO is that the question is ill-posed.

To see this, let me highlight what I think are the many implicit 
assumptions behind the question by spelling it out in great detail.  The 
question seems to be, is there a case of a *major* theorem that was first 
proved informally, *without any machine assistance whatsoever*, and then 
carefully scrutinized by a large number of human mathematicians, again 
without any machine assistance whatsoever, then declared with extremely 
high confidence to be correct by the mathematical community, and then (and 
only then) made the target of a formalization effort, at which point a 
*major* error is discovered, which *cannot be fixed*, rendering the 
problem wide open again for a substantial period of time?

As you can see, so many conditions need to be satisfied simultaneously 
that it seems rather unlikely that it has happened and we have not heard 
about it.

Of course, weaker versions of the question have a positive answer.

- Sitting in the privacy of my office trying to prove something, I
   convince myself that I have succeeded, but then when I start typing up
   the proof, I notice a gap, which leads me to do a quick calculation with
   some conventional computer algebra package; the computer turns up a
   counterexample and it's back to the drawing board.

- In the process of formalizing something in Coq or whatever, a
   mathematician discovers a slight gap in the published proof of a result,
   which however is easily fixed.

- The "theorem" in question is the correctness of some piece of widely
   used software.  It is disproved by some hacker who manages to break into
   a bunch of computer systems by discovering and exploiting a bug.

An interesting example in the other direction was Nelson's claimed proof 
of the inconsistency of PA, which he claimed to have formally verified 
with a proof assistant.  The error in the proof was later discovered by 
human mathematicians in the conventional manner.

Tim