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