This is a list of unusually long mathematical proof

Mathematical proof

In mathematics, a proof is a convincing demonstration that some mathematical statement is necessarily true. Proofs are obtained from deductive reasoning, rather than from inductive or empirical arguments. That is, a proof must demonstrate that a statement is true in all cases, without a single...

s.

, the longest mathematical proof, measured by number of published journal pages, is the classification of finite simple groups

Classification of finite simple groups

In mathematics, the classification of the finite simple groups is a theorem stating that every finite simple group belongs to one of four categories described below. These groups can be seen as the basic building blocks of all finite groups, in much the same way as the prime numbers are the basic...

 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
  Abel–Ruffini theorem
  In algebra, the Abel–Ruffini theorem states that there is no general algebraic solution—that is, solution in radicals— to polynomial equations of degree five or higher.- Interpretation :...
  
   was nearly proved by Paolo Ruffini
  Paolo Ruffini
  Paolo Ruffini was an Italian mathematician and philosopher.By 1788 he had earned university degrees in philosophy, medicine/surgery, and mathematics...
  
  , but his proof, spanning 500 pages, was mostly ignored and later, in 1824, Niels Henrik Abel
  Niels Henrik Abel
  Niels Henrik Abel was a Norwegian mathematician who proved the impossibility of solving the quintic equation in radicals.-Early life:...
  
   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
  Constructible polygon
  In mathematics, a constructible polygon is a regular polygon that can be constructed with compass and straightedge. For example, a regular pentagon is constructible with compass and straightedge while a regular heptagon is not....
  
   by Johann Gustav Hermes
  Johann Gustav Hermes
  Johann Gustav Hermes was a German mathematician.-Life:Hermes was born in Königsberg and was educated at the Kneiphöfischen Gymnasium. He undertook his Abitur at the school in 1866. After completing his secondary education, he studied mathematics from 1866 to 1870, mostly in Königsberg...
  
   took over 200 pages.
• 1905 Lasker–Noether theorem
  Lasker–Noether theorem
  In mathematics, the Lasker–Noether theorem states that every Noetherian ring is a Lasker ring, which means that every ideal can be written as an intersection of finitely many primary ideals...
  
   Emmanuel Lasker's original proof took 98 pages, but has since been simplified: modern proofs are less than a page long.
• 1963 Odd order theorem This 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
  Resolution of singularities
  In algebraic geometry, the problem of resolution of singularities asks whether every algebraic variety V has a resolution, a non-singular variety W with a proper birational map W→V...
  
   Hironaka's original proof was 216 pages long; it has since been simplified considerably down to about 10 or 20 pages.
• 1966 Discrete series representation
  Discrete series representation
  In mathematics, a discrete series representation is an irreducible unitary representation of a locally compact topological group G that is a subrepresentation of the left regular representation of G on L²...
  
  s 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
  Sergei Adian
  Sergei Ivanovich Adian, also Adjan is one of the most prominent Soviet and Russian mathematicians. He is a professor at the Moscow State University. He is most famous for his work in group theory, especially on the Burnside problem.-Biography:...
  
   proof solving Burnside's problem
  Burnside's problem
  The Burnside problem, posed by William Burnside in 1902 and one of the oldest and most influential questions in group theory, asks whether a finitely generated group in which every element has finite order must necessarily be a finite group...
  
   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
  Fondements de la Géometrie Algébrique
  FGA, or Fondements de la Géometrie Algébrique, is a book that collected together seminar notes of Alexander Grothendieck. It is animportant source for his pioneering work on scheme theory, which laid foundations for algebraic geometry in its modern technical developments.The title is a translation...
  
  , Éléments de géométrie algébrique
  Éléments de géométrie algébrique
  The Éléments de géométrie algébrique by Alexander Grothendieck , or EGA for short, is a rigorous treatise, in French, on algebraic geometry that was published from 1960 through 1967 by the Institut des Hautes Études Scientifiques...
  
   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
  Weil conjectures
  In mathematics, the Weil conjectures were some highly-influential proposals by on the generating functions derived from counting the number of points on algebraic varieties over finite fields....
  
  . While Deligne's final paper proving these was "only" about 30 pages long, it depended on background results in algebraic geometry and etale cohomology that Deligne estimated to be about 2000 pages long.
• 1974 4-color theorem. Appel and Haken's proof of this took 741 pages, and also depended on long computer calculations.
• 1974 The Gorenstein–Harada theorem
  Gorenstein–Harada theorem
  In mathematical finite group theory, the Gorenstein–Harada theorem, proved by in a 464 page paper, classifies the simple finite groups of sectional 2-rank at most 4...
  
   classifying finite groups of sectional 2-rank at most 4 was 464 pages long.
• 1976 Eisenstein series
  Eisenstein series
  Eisenstein series, named after German mathematician Gotthold Eisenstein, are particular modular forms with infinite series expansions that may be written down directly...
  
   Langlands's proof of the functional equation for Eisenstein series was 337 pages long.
• 1983 Trichotomy theorem
  Trichotomy theorem
  In mathematical finite group theory, the trichotomy theorem divides the simple groups of characteristic 2 type and rank at least 3 into three classes...
  
   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
  Selberg trace formula
  In mathematics, the Selberg trace formula, introduced by , is an expression for the character of the unitary representation of G on the space L2 of square-integrable functions, where G is a Lie group and Γ a cofinite discrete group...
  
   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–Selberg trace formula
  In mathematics, the Arthur–Selberg trace formula is a generalization of the Selberg trace formula from the group SL2 to arbitrary reductive groups over global fields, developed by James Arthur in a long series of papers from 1974 to 2003....
  
  . 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
  Lafforgue's theorem
  In mathematics, Lafforgue's theorem, due to Laurent Lafforgue, completes the Langlands program for general linear groups over function fields, by giving a correspondence between automorphic forms on these groups and representations of Galois groups....
  
   on the Langlands conjecture for the general linear group over function fields. Laurent Lafforgue
  Laurent Lafforgue
  Laurent Lafforgue is a French mathematician.He won 2 silver medals at International Mathematical Olympiad in 1984 and 1985....
  
  's proof of this was about 600 pages long, not counting many pages of background results.
• 2003 Poincaré conjecture
  Poincaré conjecture
  In mathematics, the Poincaré conjecture is a theorem about the characterization of the three-dimensional sphere , which is the hypersphere that bounds the unit ball in four-dimensional space...
  
  , Geometrization theorem
  Geometrization theorem
  In geometry, geometrization theorem may refer to*Thurstons's hyperbolization theorem for Haken 3-manifolds*Thurston's geometrization conjecture proved by Perelman, a generalization of the hyperbolization theorem to all compact 3-manifolds....
  
  , Geometrization conjecture
  Geometrization conjecture
  Thurston's geometrization conjecture states that compact 3-manifolds can be decomposed canonically into submanifolds that have geometric structures. The geometrization conjecture is an analogue for 3-manifolds of the uniformization theorem for surfaces...
  
  . 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 Quasi-thin groups The classification of the simple quasi-thin groups by Aschbacher and Smith was 1221 pages long, one of the longest single papers ever written.
• 2004 Classification of finite simple groups
  Classification of finite simple groups
  In mathematics, the classification of the finite simple groups is a theorem stating that every finite simple group belongs to one of four categories described below. These groups can be seen as the basic building blocks of all finite groups, in much the same way as the prime numbers are the basic...
  
  . 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
  Robertson–Seymour theorem
  In graph theory, the Robertson–Seymour theorem states that the undirected graphs, partially ordered by the graph minor relationship, form a well-quasi-ordering...
  
  . The proof takes about 500 pages spread over about 20 papers.
• 2005 Kepler conjecture
  Kepler conjecture
  The Kepler conjecture, named after the 17th-century German astronomer Johannes Kepler, is a mathematical conjecture about sphere packing in three-dimensional Euclidean space. It says that no arrangement of equally sized spheres filling space has a greater average density than that of the cubic...
  
   Hales
  Thomas Callister Hales
  Thomas Callister Hales is an American mathematician. He is known for his 1998 computer-aided proof of the Kepler conjecture, a centuries-old problem in discrete geometry which states that the most space-efficient way to pack spheres is in a pyramid shape...
  
  's proof of this involves several hundred pages of published arguments, together with several gigabytes of computer calculations.
• 2006 the strong perfect graph theorem
  Perfect graph
  In graph theory, a perfect graph is a graph in which the chromatic number of every induced subgraph equals the size of the largest clique of that subgraph....
  
  , by Maria Chudnovsky
  Maria Chudnovsky
  Maria Chudnovsky is an Israeli mathematician. She is professor in the departments of mathematics and of industrial engineering and operations research at Columbia University. She grew up in Russia and Israel, studying at the Technion, and received her Ph.D. in 2003 from Princeton University under...
  
  , Neil Robertson
  Neil Robertson (mathematician)
  G. Neil Robertson is a mathematician working mainly in topological graph theory, currently a distinguished professor at the Ohio State University. He earned his Ph.D. in 1969 at the University of Waterloo under his doctoral advisor William Tutte. According to the criteria of the Erdős Number...
  
  , Paul Seymour, and Robin Thomas. 180 pages in the Annals of Mathematics
  Annals of Mathematics
  The Annals of Mathematics is a bimonthly mathematical journal published by Princeton University and the Institute for Advanced Study. It ranks amongst the most prestigious mathematics journals in the world by criteria such as impact factor.-History:The journal began as The Analyst in 1874 and was...
  
  .

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
  Lyons group
  In the mathematical field of group theory, the Lyons group Ly , is a sporadic simple group of order...
  
  , originally used computer calculations with large matrices or with permutations on billions of symbols. In most cases, such as the baby monster group
  Baby Monster group
  In the mathematical field of group theory, the Baby Monster group B is a group of orderThe Baby Monster group is one of the sporadic groups, and has the second highest order of these, with the highest order being that of the 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
  Riemann hypothesis
  In mathematics, the Riemann hypothesis, proposed by , is a conjecture about the location of the zeros of the Riemann zeta function which states that all non-trivial zeros have real part 1/2...
  
   for the first 10¹³ zeros of the Riemann zeta function
• 2008 Proofs that various Mersenne numbers with around ten million digits are prime.
• Calculations of large numbers of digits of π.
• 2010 Showing that Rubik's cube
  Rubik's Cube
  Rubik's Cube is a 3-D mechanical puzzle invented in 1974 by Hungarian sculptor and professor of architecture Ernő Rubik.Originally called the "Magic Cube", the puzzle was licensed by Rubik to be sold by Ideal Toy Corp. in 1980 and won the German Game of the Year special award for Best Puzzle that...
  
   can be solved in 20 moves
  Optimal solutions for Rubik's Cube
  There are many algorithms to solve scrambled Rubik's Cubes. The maximum number of face turns needed to solve any instance of the Rubik's cube is 20. This number is also known as the diameter of the Cayley graph of the Rubik's cube group. An algorithm that solves a cube in the minimum number of...
  
  .

Long proofs in mathematical logic

Kurt Gödel

Kurt Gödel

Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...

 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

Harvey Friedman

Harvey Friedman is a mathematical logician at Ohio State University in Columbus, Ohio. He is noted especially for his work on reverse mathematics, a project intended to derive the axioms of mathematics from the theorems considered to be necessary...

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.