I am no expert in logic, but let me give it a try. There is an old (1970) theorem of M. Waldschmidt that at least one of the numbers $e^e$ and $e^{e^2}$ is transcendental. So, the statement is a disjunction $A\lor B$. To prove this in constructive logic, you need to prove either $A$ or $B$ which, for the best of my knowledge, is wide open. (Though nobody doubts that both $A$ and $B$ are true as it follows from the Schanuel conjecture.) I do not know if a proof in constructive logic would be gigantic, but this far there is no proof whatsoever. Of course, this example is still in the same direction is one given by Joel Hamkins, but personally I would not call it cheating.

I am no expert in logic, but let me give it a try. There is an old (1970) theorem of M. Waldschmidt that at least one of the numbers $e^e$ and $e^{e^2}$ is transcendental. So, the statement is a disjunction $A\lor B$. To prove this in constructive logic, you need to prove either $A$ or $B$ which, for the best of my knowledge, is wide open. (Though nobody doubts that both $A$ and $B$ are true as it follows from the Schanuel conjecture.) I do not know if a proof in constructive logic would be gigantic, but this far there is no proof whatsoever. Of course, this example is still in the same direction is one given by Joel Hamkins, but personally I would not call it cheating.

[EDIT] Wait, I think I know a better example: the Roth's theorem!

For any irrational algebraic number $\alpha$ and any $\varepsilon>0$ there is $c>0$ such that $$\left|\alpha-\frac{p}{q}\right|>\frac{c}{q^{2+\varepsilon}}$$ for all integers $q>0$ and $p$.

This is a $\Pi_2^0$ statement whose known proofs are nonconstructive. (The existence is proved by contradiction.) A constructive proof of this theorem would be really big news.