Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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

share|improve this question
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
add comment

3 Answers

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.

share|improve this answer
add comment

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.

share|improve this answer
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
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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