Nope... it depends on the language you use to write the proof. Agda proofs for instance are in R.
Is it really a proof (in the philosophical sense) if it cannot be verified in polynomial time?
Sure! Exponential time can be very small in practice. Agda proofs are proofs when the compiler stops churning.
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.
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.