[FOM] Talk on Formal Verification
di.gama at gmail.com
Wed Feb 3 12:17:13 EST 2016
On Wed, Feb 3, 2016 at 9:32 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> > Of course, ifyour community actually does certify something that later
> turns out to be flawed, and top researchers were involved, then that is a
> whole new story. I assume that that hasn't happened, at least for a
> As far as I’m aware, nobody has ever published a machine proof of a
> theorem that turned out to be false. A number of software errors have been
> reported in various systems, and it’s encouraging that generally these have
> been recognised by the users themselves.
Usually, a bug in a proving software is demonstrated to be an actual bug by
proving a contradiction. Since contradiction "turns out to be false",
doesn't this trivially satisfy the requirement, and make bugs in a prover
more or less synonymous with false formal proofs?
Taking the question less literally, I don't think there are any examples of
major results that were subtly flawed as a result of a bug, without simply
passing via the principle of explosion.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the FOM