It is said that proofs in constructive math, if possible at all, tend to be more verbose than in classical math. I'm trying to get an intuition for this, so:

Are there any good example of theorems mathematicians use, for which the proof in constructive math is considerably larger that the proof in classical math?

I'm not looking for artificial examples like in this question (https://mathoverflow.net/questions/294092/g%c3%b6dels-speed-up-from-constructive-to-classical-logic), but rather for meaningful theorems.

  • $\begingroup$ It's not a surprise constructive proofs are longer than classical proofs: every constructive proof is a classical proof and it usually proves more. $\endgroup$
    – lhf
    Commented Jan 23, 2019 at 10:32
  • 1
    $\begingroup$ @lhf: It's not a surprise indeed. But I'm wondering if there are particular cases where this fact has most impact. $\endgroup$
    – ternary
    Commented Jan 23, 2019 at 10:34
  • $\begingroup$ Most proofs in constructive math look just like proofs in classical math. That's not the same question as whether there are particular theorems that have longer constructive proofs than their classical proofs. $\endgroup$ Commented May 2, 2019 at 22:31

1 Answer 1


The proof that there are irrational numbers $a$, and $b$ such that $a^b$ is rational using $a = \sqrt{2}^\sqrt{2}$ and $b = \sqrt{2}$ is a good example. I believe it has a constructive proof that that is fairly long but the classical proof is short. However that's also a good case for showing that it need not always be that way, since there's a constructive proof that is almost as short as the non-constructive proof using $a = \sqrt{2}$ and $b = \log_2{9}$.

  • $\begingroup$ My apologies if I made the question too unclear, but if the theorem to be proven is the "there are irrational numbers $a$ and $b$ so that...", then the constructive proof is, as you say, not necessarily longer, and therefore would not be an example of what I'm looking for. If, on the other hand, it is to be proven either that $\sqrt{2}^{\sqrt{2}}$ is rational, or that it is irrational, then I don't see yet how the constructive proof would be longer than a classical one. $\endgroup$
    – ternary
    Commented May 6, 2019 at 17:24
  • $\begingroup$ Well if you look for ages you can always shorten a proof, but the difficulty expanding the proof of "there are irrational numbers $a$ and $b$ so that..." using $\sqrt{2}^\sqrt{2}$ illustrates the point I think. $\endgroup$ Commented May 7, 2019 at 19:17
  • $\begingroup$ More generally, look in a textbook of Constructive Analysis and I'm sure you can find some. $\endgroup$ Commented May 7, 2019 at 19:17
  • $\begingroup$ The problem is that constructive math textbooks don't list the classical proofs. So I was wondering whether someone who did a lot of comparative work between both would know a good example. $\endgroup$
    – ternary
    Commented May 11, 2019 at 8:28
  • $\begingroup$ Well, I think both the proof using $a=\sqrt{2}^{\sqrt{2}}$ and $b=\sqrt{2}$ and the one using $a=\sqrt{2}$ and $b=log_2 9$ are pretty much short beyond any shortening. And I would regard them as having a rather similar size (although proof size could be formalized for a less vague comparison). So you probably see that your answer, while being insightful, is not really an answer for the question about a significantly larger constructive proof for some theorem. $\endgroup$
    – ternary
    Commented May 11, 2019 at 8:32

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .