17
$\begingroup$

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.

  • 0
    @ShreevatsaR If a computer could prove exiting theorems, there would be several useful applications.For example, I would let a computer prove a proposition which I think is likely to be true, but could not come up with a proof by myself.2012-09-21

7 Answers 7

8

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.

4

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

4

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.

3

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

  • 5
    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.2012-08-31
2

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

  • 0
    You're right! Sorry.2012-09-04
1

Recently I and many colleagues have been proving theorems in combinatorics on words using the Walnut prover written by Hamoon Mousavi. Some of these theorems are quite nontrivial and for some no other proof is currently known. It has also been used to correct slightly wrong results in the literature.

For more info about Walnut, see https://arxiv.org/abs/1603.06017 .

For some of my papers on this subject see https://cs.uwaterloo.ca/~shallit/papers.html .

0

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.