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

<p>As Andrej points out though, it occasionally happens that soundness-breaking bugs <em>do</em> crop up in these systems (though usually not <em>silently</em>, 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.</p>

<p>Some examples of such library breaking proofs in Coq:</p>

<p><a href="https://coq.inria.fr/bugs/show_bug.cgi?id=4294">https://coq.inria.fr/bugs/show_bug.cgi?id=4294</a></p>

<p><a href="https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html">https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html</a></p>

<p>It's hard to say whether the established proofs <em>depended</em> 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!</p>

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

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

CC BY-SA 3.0
2017-01-16T08:00:46.650Z
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.
Andrej Bauer
CC BY-SA 3.0
2017-01-16T09:29:26.100Z
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.
Andrej Bauer
CC BY-SA 3.0
2017-01-16T19:20:18.853Z
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.)
Geoffrey Irving
CC BY-SA 3.0
2017-01-16T19:22:04.413Z
@AndrejBauer: I do like the subtly made point that it would make for an interesting *couple months*, rather than a longer period. :)
Geoffrey Irving
CC BY-SA 3.0
2017-01-16T19:22:36.240Z
@AndrejBauer: https://en.wikipedia.org/wiki/Kunen's_inconsistency_theorem ;)
cody
CC BY-SA 3.0
2017-01-16T19:26:12.477Z
@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](https://en.wikipedia.org/wiki/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...
cody
CC BY-SA 3.0
2017-01-16T19:27:02.133Z
... 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.
cody
CC BY-SA 3.0
2017-01-16T03:28:07.650Z
2017-01-16T03:28:07.650Z
cody
<p>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.</p>

<p>Three questions, in order of strength:</p>

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

<p>I'll leave the definition of "major" up to others.</p>

CC BY-SA 3.0
2017-01-13T15:55:55.333Z
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.
Sasho Nikolov
CC BY-SA 3.0
2017-01-13T16:56:09.273Z
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.
Geoffrey Irving
CC BY-SA 3.0
2017-01-13T17:12:54.360Z
@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.
Andrej Bauer
CC BY-SA 3.0
2017-01-13T17:54:26.390Z
Thanks @AndrejBauer. So "major proof" and "major theorem" here mean not major for research mathematicians but proofs of correctness of important critical systems?
Sasho Nikolov
CC BY-SA 3.0
2017-01-13T18:01:35.390Z
@SashoNikolov: I'd be happy with answers about either type of proof.
Geoffrey Irving
CC BY-SA 3.0
2017-01-13T21:26:51.587Z
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.
Andrej Bauer
CC BY-SA 3.0
2017-01-14T01:51:24.427Z
Andrej: Possibly not even maliciously, since some proof assistant upgrades break tactic scripts for entirely unrelated reasons.  Someone caught by a fixed soundness bug might think it was a tactic issue.
Geoffrey Irving
<proof-assistants><soundness>
Has a proof checker bug ever invalidated a major proof?
Geoffrey Irving
# Has a proof checker bug ever invalidated a major proof?

(Asked by: username_0 on 2017-01-13)

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.

**Tags:** proof-assistants, soundness

> **Comments:**
> **username_1**: 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.  
> **username_0**: 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.  
> **username_2**: @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.  
> **username_1**: Thanks @AndrejBauer. So "major proof" and "major theorem" here mean not major for research mathematicians but proofs of correctness of important critical systems?  
> **username_0**: @SashoNikolov: I'd be happy with answers about either type of proof.  
> **username_2**: 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.  
> **username_0**: Andrej: Possibly not even maliciously, since some proof assistant upgrades break tactic scripts for entirely unrelated reasons.  Someone caught by a fixed soundness bug might think it was a tactic issue.  

---

## 1 answers

### Answer by username_3 on 2017-01-16. Score: 11 | Accepted answer

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".

> **Comments:**
> **username_2**: 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.  
> **username_2**: 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.  
> **username_0**: 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.)  
> **username_0**: @AndrejBauer: I do like the subtly made point that it would make for an interesting *couple months*, rather than a longer period. :)  
> **username_3**: @AndrejBauer: https://en.wikipedia.org/wiki/Kunen's_inconsistency_theorem ;)  
> **username_3**: @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](https://en.wikipedia.org/wiki/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...  
> **username_3**: ... 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.  

---

