29
$\begingroup$

Most (all?) proof assistants have soundness bugs fixed on occasion. However, from those I've seen these bugs are usually difficult to come across unintentionally, and results proved before the bug is fixed generally hold up after the fix.

Three questions, in order of strength:

  1. Has such a soundness bug fix ever caused a major proof to fail, without modifying the proof?
  2. If (1) is true, were major modifications ever required to fix the proof?
  3. If (2) is true, has anyone proved a wrong major theorem due to a soundness bug?

I'll leave the definition of "major" up to others.

Improve this question
$\endgroup$
7
  • 11
    $\begingroup$ This probably shows my ignorance, but has a major theorem ever been first established with a proof assistant? Of course I know about the 4 color theorem and the Kepler conjecture, but I don't think the first proofs there used proof assistants. I am curious. $\endgroup$
    – Sasho Nikolov
    Jan 13, 2017 at 15:55
  • 1
    $\begingroup$ I believe no human had proved a compiler correct, and been correct about it, until CompCert. But you're right that this would make (3) in particular a less interesting question. $\endgroup$
    – Geoffrey Irving
    Jan 13, 2017 at 16:56
  • 4
    $\begingroup$ @SashoNikolov: that's not really relevant, since most proofs done in practice by proof assistants are not about mathematics. They are usually about software systems, or about properties of formal systems, etc. (It's only a question of time when the vast majority of proofs done on this planet are not about pure math. The robots are coming.) It would be quite annoying if, for instance, someone proved using a proof assistant that some critical system is safe, and then later it turned out that they've accidentally used an inconsistency. $\endgroup$
    – Andrej Bauer
    Jan 13, 2017 at 17:12
  • 1
    $\begingroup$ Thanks @AndrejBauer. So "major proof" and "major theorem" here mean not major for research mathematicians but proofs of correctness of important critical systems? $\endgroup$
    – Sasho Nikolov
    Jan 13, 2017 at 17:54
  • 1
    $\begingroup$ I think any proof that is considered important by sufficiently many people (mathematicians, security experts, software engineers) would count. I am afraid we're not going to find out because if anyone did stumble upon this problem, the chances are they quietly fixed it. $\endgroup$
    – Andrej Bauer
    Jan 13, 2017 at 21:26

1 Answer 1

Reset to default
11
$\begingroup$

To my knowledge, no machine checked proof of a complex mathematical development has ever been retracted.

As Andrej points out though, it occasionally happens that soundness-breaking bugs do crop up in these systems (though usually not silently, as Andrej suggests), and the fix to that bug involves some changes to existing proofs, or, more likely, of the standard library of the proof system involved.

Some examples of such library breaking proofs in Coq:

https://coq.inria.fr/bugs/show_bug.cgi?id=4294

https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html

It's hard to say whether the established proofs depended on the inconsistency, since after the fix, they required minor tweaks to be accepted by the proof checker. But this happens at each non-trivial update!

My personal opinion is that such mistakes are unlikely to happen, since the paper proof needs to be well polished before machine formalization can even be attempted.

Inconsistencies in proof frameworks usually require the heavy use of strange combinations of esoteric features, and so very rarely crop up "by accident".

Improve this answer
$\endgroup$
7
  • 4
    $\begingroup$ I was referring to people fixing problems in their proof scripts silently, or even unknowingly as Geoffrey pointed out, as a reaction to bugs in proof assistants. Of course, the inconsistencies in proof assistants are always received with an amazing level of excitement. Mathematicians should have an inconsistency in math, that would make for an interesting couple of months. $\endgroup$
    – Andrej Bauer
    Jan 16, 2017 at 8:00
  • 2
    $\begingroup$ What is it with people throwing Wikipedia links at me? @RickyDemer, would you kindly please explain your point. I have heard of Russell's paradox, you know. That was more than a 100 years ago, and it lead to some excellent mathematics. I am proposing that we're ripe for another one. $\endgroup$
    – Andrej Bauer
    Jan 16, 2017 at 9:29
  • $\begingroup$ I'll accept this answer for now, but of course I'll unaccept it if someone answers in the other direction! (Full disclosure: This was the answer I was hoping for.) $\endgroup$
    – Geoffrey Irving
    Jan 16, 2017 at 19:20
  • 1
    $\begingroup$ @GeoffreyIrving The answer is somewhat unsatisfying, since it's hard for me to prove a lack of retractions! The answer is therefore somewhat necessarily based on my lack of knowledge, though there have been so few very large scale machine formalizations that I'm at least a little confident in my reply. I've also heard that some important formalizations in the B method have been shown to have inconsistent assumptions (you need to add many axioms for non-trivial statements, and the collections of axioms taken together were subsequently shown to be... $\endgroup$
    – cody
    Jan 16, 2017 at 19:26
  • 1
    $\begingroup$ ... inconsistent). Unfortunately, I can't seem to find a reference for that, so I didn't include it in my answer. Also the formalization was about a large program, and not about pure mathematics. $\endgroup$
    – cody
    Jan 16, 2017 at 19:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.