Does every theorem have a short proof?

Question

This question is somehow based on my belief that every theorem has a short and simple proof. By "proof" I mean:

• Proving an statement
• Disproving a statement
• Proving that a statement is undecidable

Once we have formalized what we understand for a "step" in a proof, could it be proven that every theorem has a proof consisting of less than $n$ steps? If so:

• What would be the (minimal) value of $n$?
• Such a proof would be about all proofs so what would it say about itself?
• Could there be (in some sense) proofs with a non-integer number of steps?

Answer 1

Let $f(n)$ be any computable (total) function. Then there must be a theorem $T$ of length $N$ such that the shortest proof of $T$ is longer than $f(N)$ steps.

This is because, if such a $T$ did not exist, we could solve known unsolvable questions.

This result assumes the following basic fact about the "length" of proofs:

1. Given any $m$, there are only finitely many proofs of length at most $m$.
2. There exists a program which can take $m$ as input an return the list of proofs of length $m$.

Answer 2

There are infinitely many theorems, if by "theorem" we just mean "true mathematical statement". If we allow $k$ distinct kinds of step, there are only $k^n$ different proofs of length $n$ (and many of them would prove the same things over and over). So no, there's no $n$ so that every theorem can be proven in $n$ steps.

As a matter of fact, Godel's Incompleteness Theorem states that there is some true mathematical statement - "theorem" by the definition I suggested earlier - which has no proof at all, given a definition of a "step" in a proof.

On the other hand, just playing with this idea, we could say a "theorem" is a true mathematical statement for which a proof has been written down. Then there is indeed a $n$ so that every theorem has a proof of length at most $n$ - take $n$ to be the number of steps required to write the longest proof that has ever been written (probably the classification theorem for finite simple groups, but I'm not sure). But I don't think there's anything interesting to say about $n$, apart from that it's HUGE as long as your proof system is reasonably simple.

Answer 3

surely a theorem doesn't need to conform to any real quality requirements, so it could contain an huge number of steps that need to be proved, greater than any n you think of.