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


3 Answers 3


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.

  • 1
    $\begingroup$ 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. $\endgroup$ Commented Jan 14, 2013 at 16:57

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

See The Search for a Finite Projective Plane of Order 10 and The Non-existence of Finite Projective Planes of Order 10.


Your Answer

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

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