Complexity of proofs

[Timothy Y. Chow]

Andrew Winkler wrote:
> I recall hearing of a theorem that said something along the lines of 
> generic axioms give rise to theorems whose proofs are exponential in the 
> lengths of their statements. It's not clear to me how to make that 
> precise. Has anyone heard this? Any pointers you could give me for 
> tracking it down? Thanks!

Well, there's this old trick:

G: "There is no proof of G with fewer than 10^100 symbols."

Is that good enough for your purposes?

Tim