4
$\begingroup$

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?

$\endgroup$
6
  • 2
    $\begingroup$ -1 en.wikipedia.org/wiki/Computer-assisted_proof $\endgroup$
    – user53153
    Feb 10 '13 at 4:04
  • 1
    $\begingroup$ You might be interested in the book A=B by Petkovsek, Wilf, and Zeilberger. It is available online for free. $\endgroup$
    – MJD
    Feb 10 '13 at 4:54
  • 1
    $\begingroup$ @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. $\endgroup$
    – dexter04
    Feb 10 '13 at 5:00
  • 1
    $\begingroup$ 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. $\endgroup$
    – Calvin Lin
    Feb 10 '13 at 5:47
  • 1
    $\begingroup$ For the Sudoku computer proof, see here. $\endgroup$
    – azimut
    Feb 10 '13 at 18:16
4
$\begingroup$

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

$\endgroup$
3
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Thanks. got a really well documented proof. $\endgroup$
    – dexter04
    Feb 14 '13 at 12:28
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.