[FOM] formal proofs /query
Timothy Y. Chow
tchow at alum.mit.edu
Sun Oct 12 14:58:55 EDT 2014
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
More information about the FOM
mailing list