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.

  • 2
    Here are some related mathoverflow threads that might be interesting: http://mathoverflow.net/questions/95776/results-that-are-easy-to-prove-with-a-computer-but-hard-to-prove-by-hand-closed http://mathoverflow.net/questions/92148/interesting-conjectures-discovered-by-computers-and-proved-by-humans2012-08-31
  • 0
    What do you mean "proved by a computer"? I could probably write a simple script to print out a proof of any theorem that I know of. I could probably add a lot more, too.2012-08-31
  • 2
    http://math.stackexchange.com/a/189030/216742012-08-31
  • 1
    A related question: [Has any previously unknown result been proven by an automated theorem prover?](http://math.stackexchange.com/questions/181003/has-any-previously-unknown-result-been-proven-by-an-automated-theorem-prover).2012-08-31
  • 1
    Although I was the one that mentioned [the related question](http://math.stackexchange.com/questions/181003/has-any-previously-unknown-result-been-proven-by-an-automated-theorem-prover), I'd like to say that I don't think they are exact duplicates. (There is already one close vote.) The other question is only about theorems, which were new (which were proved by computers first), as the title explicitly says. This question says: *by theorems, I mean the ones you can find in an undergraduate course of mathematics*, which is a substantial difference.2012-08-31
  • 5
    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.2012-08-31
  • 1
    The question needs further elaboration. Does "proved by a computer" mean discovered *and* proved, or (completely or partially) automatically proved (but not discovered)? I presume you don't want to include *verifications*, i.e. human discovered-and-proved theorems that have been presented in a form that can be mechanically verified by a proof-checker.2012-08-31
  • 2
    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.2012-08-31
  • 1
    @AsafKaragila "Obviously no computer has proved them" How do you know? "nor it needs to." I think it's very meaningful for ATP. If no computer can prove an existing theorem, ATP is of very limited use.2012-08-31
  • 0
    Yes you're correct. It is a well-known fact that Reimann used a computer to perform most of his work. How else he would prove so many things? ...2012-08-31
  • 1
    @MakotoKato: The comment "no computer has proved them, nor it needs to" meant that no computer has proved them *first* (before humans) — of course, a computer proving a theorem already known to humans is a much different thing, and what we assumed is not what you're asking. (And "nor it needs to" is because the computer proving an already known theorem does not add any new theorem to our knowledge.)2012-09-02
  • 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.

  • 0
    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.2012-08-31
  • 2
    http://mathlab.mathlab.sunysb.edu/~bishop/classes/math401.F09/HalesMAA.pdf2012-08-31
  • 6
    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.2012-08-31
  • 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.

  • 10
    I don't think it's ATP.2012-08-31
  • 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.