Gödel's speed-up from constructive to classical logic? Gödel's speed-up theorem implies that some proofs can get significantly shortened when allowing extra axioms.  There are concrete examples of this phenomenon for instance when moving from Peano arithmetic (PA) to PA + consistency(PA), or when moving from PA to second-order arithmetic, see for instance this question.
However, I am not aware of concrete examples of such a dramatic shortening when moving from constructive logic to classical logic. 
So, is there a known example of a statement that is both true in constructive and classical logic, that has a reasonably short proof in classical logic, but such that any proof in constructive logic would be gigantic (and thus not "human-readable")? 
Ideally, an example would be a statement that would feel "concrete enough" for the average mathematician, i.e. a statement involving numbers, graphs, algebraic structures, etc. (Friedman's examples on Kruskal's tree theorem  fit the bill)
(I would also be interested in an example that has a simple proof in classical logic, that is not yet known to be true in constructive logic but such that a proof, if it exists, must be gigantic.)
Update: There are indeed ways to construct such examples as indicated below, but which feel a bit like cheating as they essentially add the extra axiom in the statement. I am more thinking of some existence theorem of the form 
"For every object x satisfying ..., there exists an object y satisfying ...".
Think Friedman's examples, Four-Color Theorem, etc. In other words, an existence theorem where every constructive proof would be gigantic, but where there exists a short nonconstructive proof. Here again, one may hack this by artificially adding something of the form "or (A or not(A))" in the statement, but of course that's not really what I have in mind, nor the sort of statement a mathematician working with classical logic would try to prove on a regular day ;-) 
 A: 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.
A: Here is a something which might be an example:
Sometimes there are statements $A$ and $A^*$ which a classical mathematician would consider equivalent and a constructive mathematician would not.  An example is the existence of a winning strategy for Hex.
$A(n):$ the game of Hex on an $n \times n$ board will never end in a draw AND there is no winning strategy for the second player (the first could steal it)
$A^*(n)$ There is a winning strategy for the first player in the game of Hex on an $n \times n$ board.
There is a short constructive proof of “$\forall n\,A(n)$ “
I think a constructive mathematician would accept that $A^*(13)$ is true but consider it possible that any  explicit strategy would be enormous.
A classical mathematician would easily accept “ $\forall n\, A^*(n)$ “ That might be unprovable constructively.
———
A variation: 
$B$ no position can end in a draw.
$B^*$ for every position is either a winning strategy for the next player or a winning strategy for the previous player.
From Wikipedia:

In 1976, Shimon Even and Robert Tarjan proved that determining whether a position in a game of generalized Hex played on arbitrary graphs is a winning position is PSPACE-complete.[12] A strengthening of this result was proved by Reisch by reducing quantified Boolean formula in conjunctive normal form to Hex played on arbitrary planar graphs.[13] In computational complexity theory, it is widely conjectured that PSPACE-complete problems cannot be solved with efficient (polynomial time) algorithms. This result limits the efficiency of the best possible algorithms when considering arbitrary positions on boards of unbounded size, but it doesn't rule out the possibility of a simple winning strategy for the initial position (on boards of unbounded size), or a simple winning strategy for all positions on a board of a particular size.

A: Here is a general method to construct numerous examples. 
Let $A$ be something that is provable constructively, but only with a very long proof. Now consider the statement
 $$A\vee \neg A$$
This has a very short proof in classical logic, but constructively, you'd have to give the proof of $A$, as $\neg A$ will have no proof. 
A: I'm not quite sure about the exact constructive content of these proofs but the following is perhaps in line with what you're looking for. 
Recall Ramsey's theorem: For any natural numbers $c, k, m$ there is a natural number $n$ so that any $c$-coloring of the complete hypergraph of $k$-tuples of $[n] = \{0,...,n-1\}$ has a monochromatic subgraph of size $m$. The standard (relatively straightforward) proof of this fact uses infinite Ramsey's theorem which itself is a consequence of Konig's lemma and requires the axiom of choice (so not constructive) but one can prove this result in PA by triple induction on $c$, $k$ and $m$. If I'm not mistaken the $n$ that you get from any such triple is in fact computable from that triple (though not in any feasible sense) so I imagine that the theorem is in fact provable constructively though with considerably more effort.
