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 [update] , 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.
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.
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:
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 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
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.
Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic.
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal systems of logic such as their expressive or deductive power. However, it can also include uses of logic to characterize correct mathematical reasoning or to establish foundations of mathematics.
In mathematics and formal logic, a theorem is a statement that has been proven, or can be proven. The proof of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of the axioms and previously proved theorems.
Gödel's incompleteness theorems are two theorems of mathematical logic that are concerned with the limits of provability in formal axiomatic theories. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of mathematics. The theorems are widely, but not universally, interpreted as showing that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible.
Hilbert's tenth problem is the tenth on the list of mathematical problems that the German mathematician David Hilbert posed in 1900. It is the challenge to provide a general algorithm that, for any given Diophantine equation, can decide whether the equation has a solution with all unknowns taking integer values.
Foundations of mathematics are the logical and mathematical framework that allows the development of mathematics without generating self-contradictory theories, and, in particular, to have reliable concepts of theorems, proofs, algorithms, etc. This may also include the philosophical study of the relation of this framework with reality.
Proof theory is a major branch of mathematical logic and theoretical computer science within which proofs are treated as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of a given logical system. Consequently, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.
Jean-Pierre Serre is a French mathematician who has made contributions to algebraic topology, algebraic geometry and algebraic number theory. He was awarded the Fields Medal in 1954, the Wolf Prize in 2000 and the inaugural Abel Prize in 2003.
Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in contrast to the ordinary mathematical practice of deriving theorems from axioms. It can be conceptualized as sculpting out necessary conditions from sufficient ones.
George Stephen Boolos was an American philosopher and a mathematical logician who taught at the Massachusetts Institute of Technology.
In mathematics, arithmetic geometry is roughly the application of techniques from algebraic geometry to problems in number theory. Arithmetic geometry is centered around Diophantine geometry, the study of rational points of algebraic varieties.
In mathematics, Kruskal's tree theorem states that the set of finite trees over a well-quasi-ordered set of labels is itself well-quasi-ordered under homeomorphic embedding.
In mathematical logic, the Paris–Harrington theorem states that a certain claim in Ramsey theory, namely the strengthened finite Ramsey theorem, which is expressible in Peano arithmetic, is not provable in this system. That Ramsey-theoretic claim is, however, provable in slightly stronger systems.
In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is proved to be impossible to construct an algorithm that always leads to a correct yes-or-no answer. The halting problem is an example: it can be proven that there is no algorithm that correctly determines whether an arbitrary program eventually halts when run.
The Brouwer–Hilbert controversy was a debate in twentieth-century mathematics over fundamental questions about the consistency of axioms and the role of semantics and syntax in mathematics. L. E. J. Brouwer, a proponent of the constructivist school of intuitionism, opposed David Hilbert, a proponent of formalism. Much of the controversy took place while both were involved with Mathematische Annalen, the leading mathematical journal of the time, with Hilbert as editor-in-chief and Brouwer as a member of its editorial board. In 1920 Hilbert had Brouwer removed from the editorial board of Mathematische Annalen.
In mathematics, the Ax–Grothendieck theorem is a result about injectivity and surjectivity of polynomials that was proved independently by James Ax and Alexander Grothendieck.
In proof theory, a branch of mathematical logic, elementary function arithmetic (EFA), also called elementary arithmetic and exponential function arithmetic, is the system of arithmetic with the usual elementary properties of 0, 1, +, ×, , together with induction for formulas with bounded quantifiers.
In mathematics, Gödel's speed-up theorem, proved by Gödel, shows that there are theorems whose proofs can be drastically shortened by working in more powerful axiomatic systems.