[bodhiandpysics1]

Nope... it depends on the language you use to write the proof. Agda proofs for instance are in R.

[bawolff]

Is it really a proof (in the philosophical sense) if it cannot be verified in polynomial time?

[klyrs]

Computing the n-th Ramsey number R(n,n) is doable in exponential time. You can easily brute-force R(4, 4); a perfectly credible proof that takes exponential time! A credible proof must be verifiable in demonstrably finite time -- not necessarily polynomial.

[fspeech]

Hard to find =/= hard to verify. Indeed that is the point of NP (which stands for "nondeterministic polynomial" time): solutions must be easy to check.

[bodhiandphysics]

Sure! Exponential time can be very small in practice. Agda proofs are proofs when the compiler stops churning.