# What are the theorems of mathematics proved by a computer so far?

By theorems, I mean the ones you can find in an undergraduate course of mathematics, not the ones you can find in a textbook of automated proofs.

I mean by "proved by a computer" that an existing theorem was fully automatically proved by a computer(Automated Theorem Proving).

I exclude verifications of existing theorems by a computer.

This is a related question.

-
Here are some related mathoverflow threads that might be interesting: mathoverflow.net/questions/95776/… mathoverflow.net/questions/92148/… – only Aug 31 '12 at 0:25
The question is fundamentally flawed. Undergrad level theorems are mostly the work of mathematicians from over a century ago. Obviously no computer has proved them, nor it needs to. – Asaf Karagila Aug 31 '12 at 13:13
I very recently wrote a program that proved on this very site that there is no continuous injection from $\mathbb R^2$ into $\mathbb R$. I wrote it in Markup and MathJax. Note that whenever you will access the proof the servers of math.SE will run the code and prove this theorem again. – Asaf Karagila Aug 31 '12 at 17:13

According to this, Robbin's problem concerning whether a Robbin's Algebra is a Boolean algebra is an important example. This was proven in 1996 by the Automated Theorem Proving system EPQ. The link contains further information.

-

There is project Mizar that aims to develop a database of formally verified mathematic theorems. The Mizar Mathematical Library contains a lot of "standard" mathematical theorems (see the link for examples). However, the theorems are not really proved automatically, the proofs are written by a human in the Mizar language and then they're verified (which at the end doesn't matter that much, the most important thing is that we have a formal proof that can be verified and manipulated by a computer).

-

One well known theorem that has been formally proven is the Jordan curve theorem.

-
I'm sorry I can't believe it. Jordan curve theorem is highly non-trivial. I don't think an existing computer can prove it. – Makoto Kato Aug 31 '12 at 6:58
I understand it's basically a translation from an informal proof(the usual proof) to a formal proof. I guess the aim was to check the proof by a computer. – Makoto Kato Aug 31 '12 at 7:17
This is an example of a known (human) proof that was translated into a formal proof that was verified by computer, not an example of "automated theorem proving" in which the computer came up with the proof by itself. – ShreevatsaR Aug 31 '12 at 10:39

I think the most-cited example is from several years ago: pons asinorum. At least that was a genuine example where the programmers were surprised of the nice proof they had not known themselves and it was likely more elegant than Euclid's original—but it turned out, it was already known to Pappus.

-

The 4-colour theorem was one of the first, if not the first.

-
I don't think it's ATP. – Makoto Kato Aug 31 '12 at 7:34
You're right! Sorry. – exfenestracide Sep 4 '12 at 7:57

Practically all, if not all, of the object language theorems for a propositional calculus in a mathematical logic course (and they do get taught in math departments, right?) have gotten proven by a theorem prover... or could fairly handily get proven with a theorem prover once one knows some strategies.

-