What are some theorems that currently only have computer-assisted proofs? For example, there's the four colour theorem.
I am very curious about this and would like to generate a list.
$\begingroup$
$\endgroup$
7
-
17$\begingroup$ Proof that of least amount of hints that sodoku puzzle needs to have unique solution $\endgroup$– KamsterDec 29, 2014 at 5:27
-
1$\begingroup$ Well,there are the 2 mathematicians in Austria and Germany who last year were able to use a computer to verify Kurt Godel's modal logical proof the existence of God. Yeah,you read that right. Don't believe me? Here, check it out for yourself. Of course, the big question is whether or not the question makes sense in the first place and Godel would be in good company if it wasn't: Rene Decartes, etc. $\endgroup$– Mathemagician1234Dec 29, 2014 at 7:03
-
5$\begingroup$ Also, the proof assumes 5 axioms. The validity of these axioms is questionable (in my humble opinion). $\endgroup$– Kyle GannonDec 29, 2014 at 7:38
-
2$\begingroup$ @KyleGannon Your remark could apply to every proof on Earth. $\endgroup$– Federico PoloniDec 29, 2014 at 10:58
-
10$\begingroup$ @FedericoPoloni: I was trying to imply that these axioms are a little loony. Did you look at the paper? $\endgroup$– Kyle GannonDec 29, 2014 at 19:12
|
Show 2 more comments
12 Answers
$\begingroup$
$\endgroup$
4
Hales' proof of Kepler's conjecture that cubic close packing is optimal uses computer checking of numerous cases.
-
6$\begingroup$ You posted this while I was writing mine. Here's mine as a comment: The Kepler Conjecture on the densest sphere packing in three-space, proved by Thomas Hales in 1998. Apparently the proof involved solving some 100,000 linear programming problems. A project to verify the proof with formal proof checking software (in this case, Isabelle and HOL Light) was completed just this year. $\endgroup$– aesDec 29, 2014 at 5:36
-
-
10$\begingroup$ @Victor, why accept an answer when the question is tagged under "big-list"? $\endgroup$ Dec 30, 2014 at 14:33
-
$\begingroup$ @user132181 - Because this could be understand by the general audience. $\endgroup$– VictorDec 30, 2014 at 15:43
$\begingroup$
$\endgroup$
The proof by C.W.H. Lam et al that there is no finite projective plane of order $10$.
$\begingroup$
$\endgroup$
1
Don't know if if this counts, but the proof that God's number (the maximum number of moves required to solve any Rubik's cube) is 20 is computer-assisted. It involves using an algorithm to solve every possible state of the Rubik's cube along to establish the upper bound of 20 along with a mathematical proof that one specific configuration, the Superflip, requires 20 moves (lower bound).
-
$\begingroup$ Althogh the site's proof, cube20.org, has been up for a while (and their proof dates to July, 2010 there), it strangely doesn't seem to mention the 2013-published paper on their proof dx.doi.org/10.1137/120867366 $\endgroup$– FizzJan 15, 2015 at 0:11
$\begingroup$
$\endgroup$
2
Tucker's proof of the existence of a chaotic strange attractor in the Lorenz equations.
For a list of other theorems proved using interval methods, see Proving Conjectures by Use of Interval Arithmetic by Andreas Frommer.
-
1
-
$\begingroup$ And a more recent one about the forced pendulum: dx.doi.org/10.1137/070695599 $\endgroup$– FizzFeb 26, 2015 at 7:16
$\begingroup$
$\endgroup$
Here's a very easily understandable one Sudoku fanatics have long claimed that the smallest number of starting clues a puzzle can contain is 17. Now a year-long calculation proves there are no 16-clue puzzles. The Minimum Sudoku problem was tacked by a computer proof by Gary McGuire , Bastian Tugemann , Gilles Civario Here's the paper of their algorithm .
answered Dec 30, 2014 at 7:14
$\begingroup$
$\endgroup$
Robbins conjecture that all Robbins algebras are Boolean algebras was first proven by a computer.
The program that found the proof was a general-purpose automated reasoning program that was only given the Robbins axioms and the negation of a condition $C$ such that $Robbins, C \vdash Boole$ has a simple proof, from which it derived a contradiction.
This makes the proof a bit different from the others here: while the other proofs are like buildings that could only be built using elephants and horses, this is a building built by an elephant. While the first buildings will look like ordinary buildings, only bigger, this one looks quite unfamiliar
$\begingroup$
$\endgroup$
Some processor designs are verified using automated theorem verification (such as ACL2 or in-house software). It's nothing romantic like the 4 color theorem, but the "theorems" are huge and practically impossible to verify by hand.
$\begingroup$
$\endgroup$
Here's one you're less likely to have come across. It answers the question of how many different slopes on the boundary of a hyperbolic 3-manifold can be exceptional (that is, Dehn filling at that slope gives a manifold that is not hyperbolic). As I understand it, the proof involved checking an upper bound on a continuous quantity (length), and it became important to know the size of the error that could be introduced by the computer.
$\begingroup$
$\endgroup$
2
Four Color Map Theorem.
From more recent and accepted proof by Robertson Sanders Seymour Thomas, JCTB 1997:
The four-colour theorem, that every loopless planar graph admits a vertex-colouring with at most four different colours, was proved in 1976 by Appel and Haken, using a computer. Here we give another proof, still using a computer, but simpler than Appel and Haken's in several respects.
Also see http://people.math.gatech.edu/~thomas/FC/fourcolor.html
We should mention that both our programs use only integer arithmetic, and so we need not be concerned with round-off errors and similar dangers of floating point arithmetic. However, an argument can be made that our `proof' is not a proof in the traditional sense, because it contains steps that can never be verified by humans.
-
2
-
$\begingroup$ @Victor, Robin Thomas writes on that page: "In particular, we have not proved the correctness of the compiler we compiled our programs on, nor have we proved the infallibility of the hardware we ran our programs on. These have to be taken on faith, and are conceivably a source of error." $\endgroup$ Dec 31, 2014 at 2:40
$\begingroup$
$\endgroup$
The evaluation of the Ramsey number R(4,5)=25 by Brendan D. McKay and Stanisław P. Radziszkowski. In human language: the complete graph on $25$ vertices is the smallest complete graph with the property that, if each edge is colored blue or red, there will either be a complete subgraph on $4$ vertices whose edges are all blue, or else there will be a complete subgraph on $5$ vertices whose edges are all red.
$\begingroup$
$\endgroup$
4
Since other answers refer to games (are these really theorems of mathematics?), how about Checkers is solved, Science 2007.
Jonathan Schaeffer and his team at the University of Alberta, Canada, have been working on their program, called Chinook, since 1989, running calculations on as many as 200 computers simultaneously. Schaeffer has now announced that they have solved the game of American checkers, which is played on an 8 by 8 board and is also known as English draughts.
The team directed Chinook so it didn't have to go through every one of the 500 billion billion (5 * 1020) possible moves. Not all losing plays needed to be analysed; instead, for each game position, Chinook needed to work out only a move that would allow it to win. In the end, only 1/5,000,000 of the moves were computed.
As Chinook has worked out all relevant lines of play, it needs virtually no time to 'think' to work out each perfect move in a game.
Checkmate for checkers, Nature 2007.
Consider the sequence board games of perfect information of increasing complexity: Tic Tac Toe < Checkers < Chess < Go (Wei Chi). Tic Tac Toe was already solved by Babbage. Checkers is solved, but chess only heuristically (eg Deep Rybka). The Go game tree is so large that it's a current frontier where tree pruning is abandoned in favor of Monte Carlo approaches.
-
2$\begingroup$ You left out the important part: perfect play by both sides leads to a draw. $\endgroup$– TonyKFeb 26, 2015 at 8:24
-
$\begingroup$ @TonyK, of course, perfect play means non-losing, but that's a basic definition, why is that the important part? $\endgroup$ Feb 26, 2015 at 14:59
-
$\begingroup$ As far as your answer is concerned, checkers could be a forced win for the first player (or even the second player). But, as it happens, the outcome is a draw. You forgot to mention this crucial fact. $\endgroup$– TonyKFeb 26, 2015 at 15:16
-
$\begingroup$ @TonyK, I reviewed some papers by Schaffer et al, searching for "forced" and only found 1 mention eg in (cs.ucr.edu/~eamonn/205/checkers.pdf) "Independent research has discovered a 10-piece database position requiring a 279-ply move sequence to demonstrate a forced win (a ply is one move by one player) (15). This is a conservative bound; the win length has not been computed for the more difficult (and more interesting) database positions." // most matches for "forced" refer to forced moves - so again, I ask, what makes forced wins a crucial factor in computer assisted proofs? $\endgroup$ Feb 27, 2015 at 4:36
$\begingroup$
$\endgroup$
Adding one more Erd˝os discrepancy conjecture puzzle. Here's an interesting video describing it with links to the paper in the comments https://www.youtube.com/watch?v=pFHsrCNtJu4
