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

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.

• 1799 The Abel–Ruffini theorem was nearly proved by Paolo Ruffini, but his proof, spanning 500 pages, was mostly ignored and later, in 1824, Niels Henrik Abel published a proof that required just six pages.
• 1890 Killing's classification of simple complex Lie algebras, including his discovery of the exceptional Lie algebras, took 180 pages in 4 papers.
• 1894 The ruler-and-compass construction of a polygon of 65537 sides by Johann Gustav Hermes took over 200 pages.
• 1905 Emanuel Lasker's original proof of the Lasker–Noether theorem took 98 pages, but has since been simplified: modern proofs are less than a page long.
• 1963 Odd order theorem by Feit and Thompson was 255 pages long, which at the time was over 10 times as long as what had previously been considered a long paper in group theory.
• 1964 Resolution of singularities. Hironaka's original proof was 216 pages long; it has since been simplified considerably down to about 10 or 20 pages.
• 1966 Abyhankar's proof of resolution of singularities for 3-folds in characteristic greater than 6 covered about 500 pages in several papers. In 2009, Cutkosky simplified this to about 40 pages.
• 1966 Discrete series representations of Lie groups. Harish-Chandra's construction of these involved a long series of papers totaling around 500 pages. His later work on the Plancherel theorem for semisimple groups added another 150 pages to these.
• 1968 the Novikov–Adian proof solving Burnside's problem on finitely generated infinite groups with finite exponents negatively. The three-part original paper is more than 300 pages long. (Britton later published a 282-page paper attempting to solve the problem, but his paper contained a serious gap.)
• 1960-1970 Fondements de la Géometrie Algébrique, Éléments de géométrie algébrique and Séminaire de géométrie algébrique. Grothendieck's work on the foundations of algebraic geometry covers many thousands of pages. Although this is not a proof of a single theorem, there are several theorems in it whose proofs depend on hundreds of earlier pages.
• 1974 N-group theorem. Thompson's classification of N-groups used 6 papers totaling about 400 pages, but also used earlier results of his such as the odd order theorem, which bring to total length up to more than 700 pages.
• 1974 Ramanujan conjecture and the Weil conjectures. While Deligne's final paper proving these conjectures were "only" about 30 pages long, it depended on background results in algebraic geometry and étale cohomology that Deligne estimated to be about 2000 pages long.
• 1974 4-color theorem. Appel and Haken's proof of this took 139 pages, and also depended on long computer calculations.
• 1974 The Gorenstein–Harada theorem classifying finite groups of sectional 2-rank at most 4 was 464 pages long.
• 1976 Eisenstein series. Langlands's proof of the functional equation for Eisenstein series was 337 pages long.
• 1983 Trichotomy theorem. Gorenstein and Lyons's proof for the case of rank at least 4 was 731 pages long, and Aschbacher's proof of the rank 3 case adds another 159 pages, for a total of 890 pages.
• 1983 Selberg trace formula. Hejhal's proof of a general form of the Selberg trace formula consisted of 2 volumes with a total length of 1322 pages.
• Arthur–Selberg trace formula. Arthur's proofs of the various versions of this cover several hundred pages spread over many papers.
• 2000 Almgren's regularity theorem. Almgren's proof was 955 pages long.
• 2000 Lafforgue's theorem on the Langlands conjecture for the general linear group over function fields. Laurent Lafforgue's proof of this was about 600 pages long, not counting many pages of background results.
• 2003 Poincaré conjecture, Geometrization theorem, Geometrization conjecture. Perelman's original proofs of the Poincaré conjecture and the Geometrization conjecture were not lengthy, but were rather sketchy. Several other mathematicians have published proofs with the details filled in, which come to several hundred pages.
• 2004 Quasithin groups. The classification of the simple quasithin groups by Aschbacher and Smith was 1221 pages long, one of the longest single papers ever written.
• 2004 Classification of finite simple groups. The proof of this is spread out over hundreds of journal articles which makes it hard to estimate its total length, which is probably around 10000 to 20000 pages.
• 2004 Robertson–Seymour theorem. The proof takes about 500 pages spread over about 20 papers.
• 2005 Kepler conjecture. Hales's proof of this involves several hundred pages of published arguments, together with several gigabytes of computer calculations.
• 2006 the strong perfect graph theorem, by Maria Chudnovsky, Neil Robertson, Paul Seymour, and Robin Thomas. 180 pages in the Annals of Mathematics.

Long computer calculations

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:

• Several proofs of the existence of sporadic simple groups, such as the Lyons group, originally used computer calculations with large matrices or with permutations on billions of symbols. In most cases, such as the baby monster group, the computer proofs were later replaced by shorter proofs avoiding computer calculations. Similarly, the calculation of the maximal subgroups of the larger sporadic groups uses a lot of computer calculations.
• 2004 Verification of the Riemann hypothesis for the first 10¹³ zeros of the Riemann zeta function.
• 2007 Verification that checkers is a draw.
• 2008 Proofs that various Mersenne numbers with around ten million digits are prime.
• Calculations of large numbers of digits of π.
• 2010 Showing that the Rubik's Cube can be solved in 20 moves.
• 2012 Showing that Sudoku needs at least 17 clues.
• 2013 Ternary Goldbach conjecture: Every odd number greater than 5 can be expressed as the sum of three primes.
• 2014 Proof of Erdős discrepancy conjecture for the particular case C=2: every ±1-sequence of the length 1161 has a discrepancy at least 3; the original proof, generated by a SAT solver, had a size of 13 gigabytes and was later reduced to 850 megabytes.
• 2016 Solving the Boolean Pythagorean triples problem required the generation of 200 terabytes of proof.^[1]
• 2017 Marijn Heule, who coauthored solution to the Boolean Pythagorean triples problem, announced a 2 petabytes long proof that the 5th Schur's number is 161.^[2]

Long proofs in mathematical logic

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 T₁, T₂, ..., T_n such that T_k 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 ¹⁰⁰⁰2, where ⁰2 = 1 and ^{n + 1}2 = 2⁽ⁿ²⁾ (tetrational growth). The statement is a special case of Kruskal's theorem and has a short proof in second order arithmetic.

See also

• List of incomplete proofs
• Proof by intimidation

References

• Krantz, Steven G. (2011), The proof is in the pudding. The changing nature of mathematical proof (PDF), Berlin, New York: Springer-Verlag, doi:10.1007/978-0-387-48744-1, ISBN 978-0-387-48908-7, MR 2789493
• Smoryński, C. (1982), "The varieties of arboreal experience", Math. Intelligencer, 4 (4): 182–189, doi:10.1007/bf03023553, MR 0685558, S2CID 125748405