Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.

share|improve this question
2  
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
2  
1  
4  
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
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. –  Asaf Karagila Aug 31 '12 at 17:13
show 7 more comments

5 Answers

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.

share|improve this answer
add comment

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

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

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

share|improve this answer
add comment

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.

share|improve this answer
add comment

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

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

Your Answer

 
discard

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.