Does every theorem have a short proof? 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?

 A: 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:


*

*Given any $m$, there are only finitely many proofs of length at most $m$.

*There exists a program which can take $m$ as input an return the list of proofs of length $m$.

A: 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.
A: 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.  
