Jump to content

List of long mathematical proofs

From Wikipedia, the free encyclopedia

This is a list of unusually long mathematical proofs. Such proofs often use computational proof methods and may be considered non-surveyable.

As of 2011, the longest mathematical proof, measured by number of published journal pages, is the classification of finite simple groups with well over 10000 pages. There are several proofs that would be far longer than this if the details of the computer calculations they depend on were published in full.

Long proofs

[edit]

The length of unusually long proofs has increased with time. As a rough rule of thumb, 100 pages in 1900, or 200 pages in 1950, or 500 pages in 2000 is unusually long for a proof.

Long computer calculations

[edit]

There are many mathematical theorems that have been checked by long computer calculations. If these were written out as proofs many would be far longer than most of the proofs above. There is not really a clear distinction between computer calculations and proofs, as several of the proofs above, such as the 4-color theorem and the Kepler conjecture, use long computer calculations as well as many pages of mathematical argument. For the computer calculations in this section, the mathematical arguments are only a few pages long, and the length is due to long but routine calculations. Some typical examples of such theorems include:

Long proofs in mathematical logic

[edit]

Kurt Gödel showed how to find explicit examples of statements in formal systems that are provable in that system but whose shortest proof is absurdly long. For example, the statement:

"This statement cannot be proved in Peano arithmetic in less than a googolplex symbols"

is provable in Peano arithmetic but the shortest proof has at least a googolplex symbols. It has a short proof in a more powerful system: in fact, it is easily provable in Peano arithmetic together with the statement that Peano arithmetic is consistent (which cannot be proved in Peano arithmetic by Gödel's incompleteness theorem).

In this argument, Peano arithmetic can be replaced by any more powerful consistent system, and a googolplex can be replaced by any number that can be described concisely in the system.

Harvey Friedman found some explicit natural examples of this phenomenon, giving some explicit statements in Peano arithmetic and other formal systems whose shortest proofs are ridiculously long (Smoryński 1982). For example, the statement

"there is an integer n such that if there is a sequence of rooted trees T1, T2, ..., Tn such that Tk has at most k+10 vertices, then some tree can be homeomorphically embedded in a later one"

is provable in Peano arithmetic, but the shortest proof has length at least 10002, where 02 = 1 and n + 12 = 2(n2) (tetrational growth). The statement is a special case of Kruskal's theorem and has a short proof in second order arithmetic.

See also

[edit]

References

[edit]
  1. ^ Lamb, Evelyn (26 May 2016). "Two-hundred-terabyte maths proof is largest ever: A computer cracks the Boolean Pythagorean triples problem — but is it really maths?". Nature.
  2. ^ Heule, Marijn J. H. (2017). "Schur Number Five". arXiv:1711.08076 [cs.LO].