<p>Another famous example is <a href="http://www.math.pitt.edu/~thales/papers/A%20Proof%20of%20the%20Kepler%20Conjecture%20%28Annals%29.pdf">Hales' proof of Kepler's conjecture</a> which had a very large computer aided component.</p>

<p>From <a href="http://en.wikipedia.org/wiki/Kepler%27s_conjecture#Hales.27_proof">Wikipedia</a>:</p>

<blockquote>
  <p>In August 1998 Hales announced that the proof was complete. At that stage it consisted of 250 pages of notes and 3 gigabytes of computer programs, data and results.</p>
</blockquote>

CC BY-SA 3.0
2013-01-14T05:03:44.600Z
2013-01-14T05:03:44.600Z
Huck Bennett
<p>This is more of a meta answer in that it is a list of lists.</p>

<ol>
<li><p><a href="http://www.math.rutgers.edu/~zeilberg/papers1.html">The papers of Doron Zeilberger</a>. He is a mathematician and his computer is listed at the coauthor Shalosh B. Ekhad on all papers where the computer played a part in deriving the results.</p></li>
<li><p><a href="http://www.informatik.uni-trier.de/~ley/pers/hd/g/Gonthier%3aGeorges.html">Work of Georges Gonthier</a>. He engineered a machine-checked proof of the four colour theorem and has been recently been working on the Feit-Thompson theorem. He recently completed the formalisation of the Odd-Order Theorem.</p></li>
<li><p><a href="http://afp.sourceforge.net/">Archive of Formal Proofs</a> contains proofs checked with Isabelle, and includes correctness theorems for algorithms, the Gauss-Jordan theorem, some order theory, category theory, and many more classical results.</p></li>
<li><p><a href="http://www.cs.ru.nl/~freek/100/">Formalizing 100 Theorems</a>, contains machine checked proofs of some famous theorems.</p></li>
</ol>

CC BY-SA 3.0
2013-01-14T16:57:23.607Z
Thanks. I should clarify that my question is not concerned about proofs verified/validated by computers after discovery, nor results where a computer played a part deriving them (of course we all use computers in our research, but eventually end up with a self-contained mathematical proof that we can't say has been "derived" by a computer). I'm looking for conjectures whose proofs were *generated* (fully or in part) by a computer.
Mahdi Cheraghchi
CC BY-SA 3.0
2013-01-14T07:08:44.007Z
2013-01-14T07:18:27.513Z
2013-01-14T07:18:27.513Z
Vijay D
<p>One example is the proof of non-existence of a <a href="http://en.wikipedia.org/wiki/Projective_plane#Finite_projective_planes">projective plane of order 10</a>.</p>

<p>See <a href="http://mathdl.maa.org/images/upload_library/22/Ford/Lam305-318.pdf">The Search for a Finite Projective Plane of Order 10</a> and <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.8684">The Non-existence of Finite Projective Planes of Order 10</a>.</p>

CC BY-SA 3.0
2013-01-14T10:22:55.557Z
2013-01-14T10:22:55.557Z
kbkb
<p>In 1996, a long-standing open problem was solved by a computer; namely, that <a href="http://en.wikipedia.org/wiki/Robbins_algebra">Robbins algebra</a> and Boolean algebra are the same. The proof was found by an automated theorem prover.</p>

<p>Moreover, the known proof of Four color theorem contains computer-generated components.</p>

<p>The aim of this question is to list proofs that are (completely or partially) found by computer (whether the only known proof or the one discovered for the <em>first</em> time). </p>

CC BY-SA 3.0
2013-01-14T10:55:32.733Z
Some sporadic finite simple groups (like the [Lyons group](http://en.wikipedia.org/wiki/Lyons_group) were first constructed using a computer, i.e., their existence proof was (partially) computer-generated.
j.p.
CC BY-SA 3.0
2013-01-14T12:29:22.527Z
The question [Is "Exporimental Complexity Theory" being used to solve open problems](http://cstheory.stackexchange.com/questions/524/is-experimental-complexity-theory-being-used-to-solve-open-problems/527#527) is related to this one.
adrianN
CC BY-SA 3.0
2013-01-14T12:30:47.053Z
IMHO you need to distinguish more carefully between "found" and "checked". Gonthier et al.'s proof has definitely not been found by a computer.
gallais
CC BY-SA 3.0
2013-01-14T16:18:12.263Z
nice question but alas nearly equivalent to [where & how did computers help prove a thm](http://cstheory.stackexchange.com/questions/82/where-and-how-did-computers-help-prove-a-theorem)
vzn
CC BY-SA 3.0
2013-01-20T16:53:38.127Z
Also very similar: [Has any previously unknown result been proven by an automated theorem prover?](http://math.stackexchange.com/q/181003/37490).
Petr
<soft-question><big-list><proofs><automated-theorem-proving>
Proofs found by computer
Mahdi Cheraghchi
# Proofs found by computer

(Asked by: username_0 on 2013-01-14)

In 1996, a long-standing open problem was solved by a computer; namely, that [Robbins algebra](http://en.wikipedia.org/wiki/Robbins_algebra) and Boolean algebra are the same. The proof was found by an automated theorem prover.

Moreover, the known proof of Four color theorem contains computer-generated components.

The aim of this question is to list proofs that are (completely or partially) found by computer (whether the only known proof or the one discovered for the *first* time).

**Tags:** soft-question, big-list, proofs, automated-theorem-proving
> **Comments:**
> **username_1**: Some sporadic finite simple groups (like the [Lyons group](http://en.wikipedia.org/wiki/Lyons_group) were first constructed using a computer, i.e., their existence proof was (partially) computer-generated.  
> **username_2**: The question [Is "Exporimental Complexity Theory" being used to solve open problems](http://cstheory.stackexchange.com/questions/524/is-experimental-complexity-theory-being-used-to-solve-open-problems/527#527) is related to this one.  
> **username_3**: IMHO you need to distinguish more carefully between "found" and "checked". Gonthier et al.'s proof has definitely not been found by a computer.  
> **username_4**: nice question but alas nearly equivalent to [where & how did computers help prove a thm](http://cstheory.stackexchange.com/questions/82/where-and-how-did-computers-help-prove-a-theorem)  
> **username_5**: Also very similar: [Has any previously unknown result been proven by an automated theorem prover?](http://math.stackexchange.com/q/181003/37490).  

---

## 3 answers

### Answer by username_6 on 2013-01-14. Score: 12

Another famous example is [Hales' proof of Kepler's conjecture](http://www.math.pitt.edu/~thales/papers/A%20Proof%20of%20the%20Kepler%20Conjecture%20%28Annals%29.pdf) which had a very large computer aided component.

From [Wikipedia](http://en.wikipedia.org/wiki/Kepler%27s_conjecture#Hales.27_proof):

> In August 1998 Hales announced that the proof was complete. At that stage it consisted of 250 pages of notes and 3 gigabytes of computer programs, data and results.


---

### Answer by username_7 on 2013-01-14. Score: 10

This is more of a meta answer in that it is a list of lists.

1. [The papers of Doron Zeilberger](http://www.math.rutgers.edu/~zeilberg/papers1.html). He is a mathematician and his computer is listed at the coauthor Shalosh B. Ekhad on all papers where the computer played a part in deriving the results.
2. [Work of Georges Gonthier](http://www.informatik.uni-trier.de/~ley/pers/hd/g/Gonthier%3aGeorges.html). He engineered a machine-checked proof of the four colour theorem and has been recently been working on the Feit-Thompson theorem. He recently completed the formalisation of the Odd-Order Theorem.
3. [Archive of Formal Proofs](http://afp.sourceforge.net/) contains proofs checked with Isabelle, and includes correctness theorems for algorithms, the Gauss-Jordan theorem, some order theory, category theory, and many more classical results.
4. [Formalizing 100 Theorems](http://www.cs.ru.nl/~freek/100/), contains machine checked proofs of some famous theorems.

> **Comments:**
> **username_0**: Thanks. I should clarify that my question is not concerned about proofs verified/validated by computers after discovery, nor results where a computer played a part deriving them (of course we all use computers in our research, but eventually end up with a self-contained mathematical proof that we can't say has been "derived" by a computer). I'm looking for conjectures whose proofs were *generated* (fully or in part) by a computer.  

---

### Answer by username_8 on 2013-01-14. Score: 6

One example is the proof of non-existence of a [projective plane of order 10](http://en.wikipedia.org/wiki/Projective_plane#Finite_projective_planes).

See [The Search for a Finite Projective Plane of Order 10](http://mathdl.maa.org/images/upload_library/22/Ford/Lam305-318.pdf) and [The Non-existence of Finite Projective Planes of Order 10](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.8684).


---

