List of long mathematical proofs
This is a list of unusually long mathematical proofs. Such proofs often use computational proof methods and may be considered non-surveyable. , 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: 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: 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 can not 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 . For example, the statement is provable in Peano arithmetic, but the shortest proof has length at least "A"(1000), where "A"(0)=1 and "A"("n"+1)=2. The statement is a special case of Kruskal's  theorem and has a short proof in second order arithmetic.