4

I recently read about the 4 color theorem and that it was proved using help from computers. Does anybody know of some other 'good' computer-assisted proofs apart from the 4 color theorem?

dexter04
  • 1,971
  • 2
    -1 http://en.wikipedia.org/wiki/Computer-assisted_proof –  Feb 10 '13 at 04:04
  • 1
    You might be interested in the book A=B by Petkovsek, Wilf, and Zeilberger. It is available online for free. – MJD Feb 10 '13 at 04:54
  • 1
    @5PM: I can wiki 90% of the big-list on this site. But the answers here usually have personal opinions, which I can't find on wiki. Wiki doesn't tell me which is the best way to start a subject, or how highly people think of a paper. That is why I have asked it here. – dexter04 Feb 10 '13 at 05:00
  • 1
    There is a recent paper that you need at least 17 clues in Sudoku to ensure a unique solution. It was done through brute force computation, for 5 billion cases. – Calvin Lin Feb 10 '13 at 05:47
  • @CalvinLin: can you give the name or reference of the paper you are talking about? – dexter04 Feb 10 '13 at 06:14
  • 1
    For the Sudoku computer proof, see here. – azimut Feb 10 '13 at 18:16

3 Answers3

4

The proof of Kepler's Conjecture by Tom Hales.

It is interesting because the initial informal mathematical proof with the help of some computer programs was considered "99% correct" by some journal reviewers after a few years of banging their head with it, which then motivated Hales to start a project to get it all computer-verified: proper formal machine-checked proofs. See the Flyspeck Project

Makarius
  • 173
3

The arguably second most famous computer proof in Mathematics is the one by Clement Lam showing that there is no projective plane of order 10. The computer part was a huge case-by-case analysis disproving the existence of a certain self-orthogonal code.

azimut
  • 22,696
2

The proof of The Robbins Conjecture. I find this interesting because the proof was not the computer checking thousands of cases, it was the computer coming up with a relatively simple algebraic proof. My understanding is that the problem was so removed from human intuition and so syntactic in nature that a computer was better able to find a solution just by cleverly searching the space of proofs.

You can see a version of the proof here written up by Allen Mann.

Martin Leslie
  • 1,456