MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I recall hearing about a result, or maybe a cluster of results, in some area of complexity theory, probably algebraic, to the effect that there are known, specific, short formulas whose minimal derivation is known to be exceedingly long. Or perhaps it is a specific function that requires an exceedingly deep curcuit. The "philosophy" seemed to be that such examples would threaten to make the older asymptotic question obsolete: "Who cares about asymptotics if the constants are huge." Can anyone, given these hints, describe ( and direct me to) the result I overheard?

share|cite|improve this question
Probably this question will be best addressed at I recall that kind of result, but almost certainly it is not in the book Algebraic Complexity Theory by Bürgisser et al. – Diego de Estrada Aug 19 '10 at 18:26
Honestly I think that a separate CS theory site could be a mistake. It should be fine to ask the question here and there should at least be a tool to move questions. – Greg Kuperberg Aug 19 '10 at 18:30
Actually, I posted a second question a few minutes after this one, the second on homotopy-theory and geometry. Careful consideration will reveal that the two questions are nearly identical. This illistrates the impossiblility of defining computer science as seperate from mathematics. – michael freedman Aug 20 '10 at 0:05
Greg, I hope your skepticism won't prevent you from visiting from time to time :) – Suresh Venkat Aug 20 '10 at 3:31
up vote 3 down vote accepted

Perhaps you were told about

Larry J. Stockmeyer, Albert R. Meyer: Cosmological lower bound on the circuit complexity of a small problem in logic. J. ACM 49(6): 753-784 (2002)

From the abstract: "An exponential lower bound on the circuit complexity of deciding the weak monadic second-order theory of one successor (WS1S) is proved. Circuits are built from binary operations, or 2-input gates, which compute arbitrary Boolean functions. In particular, to decide the truth of logical formulas of length at most 610 in this second-order language requires a circuit containing at least $10^{125}$ gates. So even if each gate were the size of a proton, the circuit would not fit in the known universe.

This demonstrates a specific function for which all inputs of size 610 cannot be determined within the physical universe. The proof is essentially a diagonalization argument, but is very carefully executed to take all constants into account.

(Note this is actually based on an asymptotic result, but it took some work to get a concrete lower bound out of it.)

share|cite|improve this answer
Thank you. I think this is what I had heard. Many of the other answers were quite interseting as well. Mike – michael freedman Aug 23 '10 at 16:31

The general fact surrounding some of the other answers is the following:

Every computably axiomatizable consistent theory $T$ containing trivial arithmetic admits very short theorems requiring extremely long proofs.

The basic fact is that there can be no total computable bound on the length of the proof required. To see this, suppose that there is a computable total function $f$ such that whenever statement $\psi$ is a statement of size at most $n$ provable from $T$, then there is a proof of size at most $f(n)$. In this case, the question of whether $T$ proves $\psi$ will be decidable, since we can simply inspect all proofs of length $f(n)$, where $n=|\psi|$ and check if any of them are proofs of $\psi$. But it is impossible that $T$ proves $\psi$ is decidable, since we could then produce a consistent completion of $T$, by the usual process of completing a theory, which is effective for decidable theories. This would produce a computable complete consistent theory of arithmetic, in contradiction to the incompleteness theorem.

One can make the conclusion fairly concrete via the halting problem. If $T$ is true and contains some trivial arithmetic, then $T$ will prove all true instances of the assertion program $p$ halts on input $m$, and prove no false instances. If there were a total computable function $f(p,m)$ such that whenever $p$ halted on input $m$, then there was a proof of this of length at most $f(p,m)$, then we could decide the halting problem: on input $(p,m)$, compute $f(p,m)$ and then look at all proofs of that length and determine if there is a proof of halting or not.

In conclusion:

Theorem. For any computably axiomatizable true theory $T$ and for any total computable function $f$, there is a program $p$ and input $m$ such that $T$ proves that $p$ halts on input $m$, but there is no proof of this in fewer than $f(p,m)$ steps.

Since as we all know, the computable functions can grow quite outrageously, this means that for any theory there will be short theorems that require extremely long proofs.

share|cite|improve this answer

This is a result due to Godel in his 1936 paper "Uber die Lange von Beweisen" (on the lengths of proofs), republished in English translation in volume 1 of his collected works. Roughly speaking, he shows that there are short theorems that have extremely long shortest proofs in certain formal systems, but much shorter proofs in more powerful systems. Harvey Friedman found some rather dramatic explicit examples, described by Smorynski in The varieties of arboreal experience

share|cite|improve this answer
C. Smoryński says, in the article Richard cites,: "There are many incompleteness and independence results in modern logic. [...] The exciting thing [in 1985] about the Paris-Harrington theorem [...] is that it is of the form $\forall k \exists n A(k,n)$ and is undecidable for a different reason." And then my authority to access this document is (frustratingly!) exceeded. – Joseph O'Rourke Aug 21 '10 at 0:13
There is an integer n such that if T<sub>1</sub>,...,T<sub>n</sub> is a sequence of trees with T<sub>i</sub> having cardinality at most 10+i, then some tree can be homeomorphically embedded in a later one. Friedman shows that this is provable in Peano arithmetic, but the shortest proof has length at least 2<sup>2<sup>2<sup>...</sup></sup></sup> where the tower of exponent has height 1000 – Richard Borcherds Aug 21 '10 at 19:54

Are you by any chance referring to examples like Haken's proof that the pigeonhole principle requires exponentially long resolution proofs ?

share|cite|improve this answer
G. Turán, "Resolution proofs of generalized pigeonhole principles" [Theoretical Computer Science Volume 62, Issue 3, December 1988, Pages 311-317], from the Abstract: "We extend results of Haken to give an exponential lower bound on the size of resolution proofs for propositional formulas encoding a generalized pigeonhole principle." – Joseph O'Rourke Aug 20 '10 at 15:04
Thanks, Joe. I didn't know about the more recent reference. – Suresh Venkat Aug 20 '10 at 15:22

It's clear from the space and time hierarchy theorems in computational complexity, and more specifically non-deterministic time hierarchy theorems, that there are statements with extremely long proofs in any formal system that: (1) can describe Turing machines or cellular automata or similar; (2) can describe large numbers; and (3) has proofs that can be checked in a reasonable amount of time, such as polynomial time or even exponential time. The non-deterministic hierarchy theorem says that $\text{NTIME}(f(n)) \ne \text{NTIME}(g(n))$ if $f(n)$ and $g(n)$ are reasonably separated functions. A fairly precise version of this result is due to Cook, but if $f(n)$ and $g(n)$ are far enough apart, you can conclude that there is a separation just by comparison to deterministic time. The corollary then is that you can turn instances of such a slow computational problem into a claim which cannot have a short proof; if it did have a short proof, you could find it quickly to answer the computational question.

For example, for each fixed $n$, you can take a question of the form, "can the following unit squares with teeth and notches added tile a square of size $A(n)$, the Ackermann function?" The answer is always provably yes or provably no, because it is a finite question. You can use a diagonalization argument in the sense of complexity theory to show that sometimes the proof has an Ackermann-like length.

Actually Mike sent me his question by e-mail, but I didn't think of this answer then and suggested posting the question here. I don't know if this is the result sought, or merely a similar result. I also don't see a way to convincingly argue that asymptotic results are obsolete. It is true that because some computational problems are asymptotically slow, you can make a sequence of computational problems that are all asymptotically fast, but with a worse and worse constant factor.

share|cite|improve this answer

Establishing that minimal proofs (or "derivations") of certain statements or theorems are long, is the prime target of the area called proof complexity. Concerning examples given in prior answers, like Haken's size lower bound on proofs of the pigeonhole principle, they deal with propositional logic only. Therefore, they are asymptotic results of the form: "there exists a constant $ 0<\epsilon<1 $ such that any resolution refutation of the propositional pigenohole principle $ PHP_n$ must be of length (i.e., number of steps) at least $ 2^{n^\epsilon}$"; Where $ PHP_n \;$, $ n=1,2,\ldots ,$ is an infinite family of propositional contradictions (expressing the $ n+ 1 $ to $ n\; $ pigeonhole principle). So propositional proof complexity does not seem to answer the question about non-asymptotic lower bounds.

On the other hand, lower bounds on first order proofs (having quantifiers, i.e., not propositional logic) are not necessarily asymptotic, and if this is what you are looking for, the only thorough survey I know of (dealing with both propositional and non-propositional) proof complexity is: Pavel Pudlak: The lengths of proofs, in Handbook of Proof Theory, S.R. Buss ed., Elsevier, 1998, pp.547-637, available here

(There is also an older book by Orevkov on non-propositional proof complexity: [1993] Complexity of Proofs and Their Transformations in Axiomatic theories, vol. 128 of Translations of Mathematical Monographs, American Mathematical Society, Providence, Rhode Island.)

share|cite|improve this answer

I found a citation to this paper by Joel Spencer: "Short Theorems with Long Proofs" [Amer. Math. Monthly 90(6) 365-366 (1983)]. But I do not have access to it at the moment. Certainly seems relevant from the title!

Edit. But apparently, not according to michael's comment. The abstract of this paper by Marian Mrozek, "Inheritable Properties and Computer Assisted Proofs in Dynamics" says

Since there exist short theorems having arbitrarily long proofs (a consequence of G"odel's incompletness theorems, see [4, 6, 23]) ...

Reference [4] is Spencer's paper. So I guess this just confirms that this is common knowledge, without providing the explicit example you seek. Apologies for the distraction!

share|cite|improve this answer
Thank you for the reference, but the author only remindes the reader of Godel's incompleteness theorem. No example is produced with which requires a long proof ( within some system.) – michael freedman Aug 19 '10 at 23:56

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.