# Proofs found by computer

In 1996, a long-standing open problem was solved by a computer; namely, that 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).

• Some sporadic finite simple groups (like the Lyons group were first constructed using a computer, i.e., their existence proof was (partially) computer-generated. – j.p. Jan 14 '13 at 10:55
• The question Is "Exporimental Complexity Theory" being used to solve open problems is related to this one. – adrianN Jan 14 '13 at 12:29
• 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 Jan 14 '13 at 12:30
• nice question but alas nearly equivalent to where & how did computers help prove a thm – vzn Jan 14 '13 at 16:18
• – Petr Pudlák Jan 20 '13 at 16:53

Another famous example is Hales' proof of Kepler's conjecture which had a very large computer aided component.

From Wikipedia:

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.

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

1. The papers of Doron Zeilberger. 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. 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 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, contains machine checked proofs of some famous theorems.

• 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. – MCH Jan 14 '13 at 16:57

One example is the proof of non-existence of a projective plane of order 10.