There are theorems whose shortest proof is insanely long. In 1936 Kurt Gödel published an abstract called “On the length of proofs”, which makes essentially this claim.
But what does ‘insanely long’ mean?
To get warmed up, let’s talk about some long proofs.
You’ve surely heard of the quadratic formula, which lets you solve
with the help of a square root:
There’s a similar but more complicated ‘cubic formula’ that lets you solve cubic equations, like this:
The cubic formula involves both square roots and cube roots. There’s also a ‘quartic formula’ for equations of degree 4, like this:
The quartic formula is so long that I can only show it to you if I shrink it by an absurd amount:
(Click repeatedly to enlarge.) But again, it only involves additions, subtraction, multiplication, division and taking roots.
In 1799, Paolo Ruffini proved that there was no general solution using radicals for polynomial equations of degree 5 or more. But his proof was 500 pages long! As a result, it was “mostly ignored”. I’m not sure what that means, exactly. Did most people ignore it completely? Or did everyone ignore most of it? Anyway, his argument seems to have a gap… and later Niels Abel gave a proof that was just 6 pages long, so most people give the lion’s share of credit to Abel.
Jumping ahead quite a lot, the longest proof written up in journals is the classification of finite simple groups. This was done by lots of people in lots of papers, and the total length is somewhere between 10,000 and 20,000 pages… nobody is exactly sure! People are trying to simplify it and rewrite it. The new proof will be a mere 5,000 pages long. So far six books have been written as part of this project.
Even when it’s all in one book, how can we be sure such a long proof is right? Some people want to use computers to make the argument completely rigorous, filling in all the details with the help of a program called a ‘proof assistant’.
The French are so sexy that even their proof assistant sounds dirty: it’s called Coq. Recently mathematicians led by George Gonthier have used Coq to give a completely detailed proof of a small piece of the classification of finite simple groups: the Feit–Thompson Theorem. Feit and Thompson’s original proof of this result, skipping lots of steps that are obvious to experts, took 255 pages!
What does the Feit–Thompson theorem say? Every finite group with an odd number of elements is solvable! Explaining that statement might take quite a while, depending on what you know about math. So let me just say this:
Galois invented group theory and used it to go further than Abel and Ruffini had. He showed a bunch of specific polynomial equations couldn’t be solved just using addition, subtraction, multiplication, division and taking roots. For example, those operations aren’t powerful enough to solve this equation:
while they can solve this one:
Galois showed that every polynomial equation has a group of symmetries, and you can solve the equation using addition, subtraction, multiplication, division and taking roots if its group has a certain special property. So, this property of a group got the name ‘solvability’.
Every finite group with an odd number of elements is solvable. It’s quick to say, but hard to show—so hard that making the proof fully rigorous on a computer seemed out of reach at first:
When Gonthier first suggested a formal Feit-Thompson Theorem proof, his fellow members of the Mathematical Components team at Inria could hardly believe their ears.
“The reaction of the team the first time we had a meeting and I exposed a grand plan,” he recalls ruefully, “was that I had delusions of grandeur. But the real reason of having this project was to understand how to build all these theories, how to make them fit together, and to validate all of this by carrying out a proof that was clearly deemed to be out of reach at the time we started the project.”
It took them 6 years! The completed computer proof has 170,000 lines. It involves 15,000 definitions and 4,300 lemmas. Maybe now Gonthier is dreaming of computerizing the whole classification of finite simple groups.
But there are even longer proofs of important results in math. These longer proofs all involve computer calculations. For example, Thomas Hales seems to have proved that the densest packing of spheres in 3d space is the obvious one, like this:
(There are infinitely many other equally dense packings, as I explained earlier, but none denser.)
Hales’ proof is a hundred pages of writing together with about 3 gigabytes of computer calculations. If we wrote out those calculations in a text file, they’d fill about 2 million pages!
The method is called ‘proof by exhaustion’, because it involves reducing the problem to 10,000 special cases and then settling each one with detailed calculations… thus exhausting anybody who tries to check the proof by hand. Now Hales is trying to create a fully formal proof that can be verified by automated proof checking software such as HOL. He expects that doing this will take 20 years.
These proofs are long, but they’re not what I’d call insanely long.
What do I mean by ‘insanely’ long? Well, for example, I know a theorem that you can prove using the usual axioms of arithmetic—Peano arithmetic—but whose shortest proof using those axioms contains
symbols. This is so many symbols that you couldn’t write them all down if you wrote one symbol on each proton, neutron and electron in the observable Universe!
I also know a theorem whose shortest proof in Peano arithmetic contains
symbols. This is so many that if you tried to write down the number of symbols—not the symbols themselves—in ordinary decimal notation, you couldn’t do it if you wrote one digit on each proton, neutron and electron in the observable Universe!
I also know a theorem whose shortest proof in Peano arithmetic contains…
… well, you get the idea.
By the way, if you don’t know what Peano arithmetic is, don’t worry. It’s just a list of obvious axioms about arithmetic, together with some obvious rules for reasoning, which turn out to be good enough to prove most everyday theorems about arithmetic. The main reason I mention it is that we need to pick some particular setup before we can talk about the ‘shortest proof’ of a theorem and have it be well-defined.
Also by the way, I’m assuming Peano arithmetic is consistent. If it were inconsistent, you could prove 0=1, and then everything would follow quite quickly from that. But most people feel sure it’s consistent.
If it is, then the shortest proof using Peano arithmetic of the following theorem contains at least 
This statement has no proof in Peano arithmetic that contains fewer than
Huh? This doesn’t look a statement about arithmetic! But Gödel showed how you could encode the concept of ‘statement’ and ‘proof’ into arithmetic, and use this to create statements that refer to themselves. He’s most famous for this one:
This statement has no proof in Peano arithmetic.
It turns out that this statement is true… so it’s an example of a true statement about arithmetic that can’t be proved using Peano arithmetic! This is Gödel’s first incompleteness theorem.
This variation is similar:
This statement has no proof in Peano arithmetic that contains fewer than
This statement is also true. It’s provable in Peano arithmetic, but its proof contains at least
But this is just the beginning. If Peano arithmetic is consistent, there are infinitely many theorems whose shortest proof is longer than 10 to the 10 to the 10 to the 10 to the… where the stack of 10’s is as long as the statement of the theorem.
Indeed, take any computable function, say F—growing as fast as you like. Then if Peano arithmetic is consistent, there are infinitely many theorems whose shortest proof is longer than this function of the length of the theorem!
But how do we know this? Here’s how. Using Gödel’s clever ideas, we can create a statement in arithmetic that says:
This statement has no proof in Peano arithmetic that is shorter than F of the length of this statement.
Let’s call this statement P.
We’ll show that if Peano arithmetic is consistent, then P is provable in Peano arithmetic. So, according to what P itself says, P is an example of a statement whose shortest proof is insanely long!
Now, let me sketch why if Peano arithmetic is consistent then P is provable in this setup. To save time, I’ll use N to stand for ‘F of the length of P’. So, P says:
P has no proof in Peano arithmetic whose length is less than N.
Assume there were a proof of P in Peano arithmetic whose length is less than N. Then, thanks to what P actually says, P would be false.
Moreover, we could carry out the argument I just gave within Peano arithmetic. So, within Peano arithmetic, we could disprove P.
But wait a minute—this would mean that within Peano arithmetic we could both prove and disprove P! We’re assuming Peano arithmetic is consistent, so this is impossible.
So our assumption must have been wrong. P must have no proof in Peano arithmetic whose length is less than N.
But this is what P says! So P is true!
Even better, P is provable in Peano arithmetic. Why? Because we can just go through all proofs shorter than N, and check that they’re not proofs of P… we know they won’t be… and this will constitute a proof that:
P has no proof in Peano arithmetic whose length is less than N.
But this is just what P says! So this is a way to prove P. Moreover we can carry out this long-winded check within Peano arithmetic, and get a proof of P in Peano arithmetic!
Of course, this proof has length more than N.
By the way, here I’m using the fact that there are only finitely many proofs with length less than N, so we can go through them all. We have to define ‘length’ in a way that makes this true, for my argument to work. For example, we can take the length to be the number of symbols.
Also, it’s important that our function F be computable. We need to compute N to know how many proofs we need to go through.
The upshot: if Peano arithmetic is consistent, there’s a provable statement whose shortest proof in Peano arithmetic is insanely long, by any computable standard of what counts as ‘insanely long’.
Now, so far we’ve just gotten one theorem with an insanely long proof. But we can get infinitely many, one for each natural number n, as follows. Let P(n) be a statement in arithmetic that says:
This statement has no proof in Peano arithmetic whose length is less than n plus F of the length of this statement.
The same argument I just sketched shows that if Peano arithmetic is consistent then P(n) is provable, but has no proof shorter than n plus F of the length of P(n). The statements P(n) are different for different values of n. So, we get infinitely many different statements with insanely long proofs… at least if Peano arithmetic is consistent, which most people believe.
But wait a minute! If we’ve proved all these statements P(n) have proofs, then we’ve basically proved them—no? And my argument, though sketchy, was quite short. So, even a completely detailed version of my argument should not be ‘insanely long’. Doesn’t that contradict my claim that the shortest proofs of these statements are insanely long?
Well, no. I only showed that the shortest proof of P(n) using Peano arithmetic is insanely long. I did provide a short proof of P(n). But I did this assuming Peano arithmetic is consistent!
So I didn’t give a short proof of P(n) using Peano arithmetic. I gave a short proof using Peano arithmetic plus the assumption that Peano arithmetic is consistent!
So, if we add to Peano arithmetic an extra axiom saying ‘Peano arithmetic is consistent’, infinitely many theorems get vastly shorter proofs!
This is often called Gödel’s speedup theorem. For more, see:
• Gödel’s speedup theorem, Wikipedia.
It’s pretty cool how just knowing Peano arithmetic was consistent would let us vastly shorten infinitely many proofs.
As an instant consequence, we get Gödel’s second incompleteness theorem: it’s impossible to use Peano arithmetic to prove its own consistency. For if we could, adding that consistency as an extra axiom couldn’t shorten proofs by an arbitrarily large amount. It could only shorten proofs by a fixed finite amount: roughly, the number of symbols in the proof that Peano arithmetic is consistent.
And while we’re at it, let’s note how the existence of insanely long proofs is related to another famous result: the Church–Turing theorem. This says it’s impossible to write a computer program that can decide in a finite time, yes or no, whether any given statement is provable in Peano arithmetic.
Suppose that in Peano arithmetic there were a computable upper bound on the length of a proof of any statement, as a function of the length of that statement. Then we could write a program that would go through all potential proofs of any statement and tell us, in a finite amount of time, whether it had a proof. So, Peano arithmetic would be decidable!
But since it’s not decidable, no such computable upper bound can exist. This is another way of seeing that there must be theorems with insanely long proofs.
So, the existence of insanely long proofs is tightly connected to the inability of Peano arithmetic to prove itself consistent, and also the undecidability of Peano arithmetic. And these are features not just of Peano arithmetic, but of any system of arithmetic that’s sufficiently powerful, yet simple enough that we can write a program to check to see if a purported proof really is a proof.
In fact Gödel stated his result in a more sophisticated way than I did. He never published a proof… but not because the proof is insanely long, probably just because he was a busy man with many ideas. Samuel Buss gave a proof in 1994:
• On Gödel’s theorems on lengths of proofs I: Number of lines and speedups for arithmetic, Journal of Symbolic Logic 39 (1994), 737–756.
In first-order arithmetic you can use variables like x,y,z to stand for natural numbers like 0,1,2,3,… This is the kind of arithmetic I’ve been talking about so far: Peano arithmetic is an example. In second-order arithmetic you can also use variables of a different kind to stand for sets of natural numbers. Third-order arithmetic goes further and lets you use variables for sets of sets of natural numbers, and so on.
Gödel claimed, and Buss showed, that each time you go up an order, some statements that were already provable get insanely shorter proofs. So, turning this fact around, there are theorems that have insanely long proofs in first-order arithmetic!
(And similarly for second-order arithmetic, and so on…)
For more details, explained in a fairly friendly way, try:
• Speed-up theorems, Stanford Encyclopedia of Philosophy.
By the way, this post is a kind of followup to my post on enormous integers. Insanely long proofs are related to enormous integers: if you know a quick way to describe an enormous integer, you can use the trick I described to cook up a theorem with an enormous proof.
Last time we saw the logician Harvey Friedman was a master of enormous integers. So it’s not surprising to me that Wikipedia says:
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.
However, I don’t know these statements. I assume they’re more natural than the weird self-referential examples I’ve described. What are they?
]]>
