# List of long proofs

This is a list of unusually long mathematical proofs.

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.

## 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 1013 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 can be solved in 20 moves.

## 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).