constructive-mathematics
$\sqrt{2}^{2\log_2 3} = 3$ is a solution to Can an irrational number raised to an irrational power be rational?
While the famous $\sqrt{2}^{\sqrt{2}}$ proof is nonconstructive, this one is apparently constructive.
However, it is not clear to me that the existence of $\log_2 3$ can be proved without the use of the principle of excluded middle. The proof I know is using the intermediate value theorem on $2^0<3<2^2$, but I think it requires the principle of excluded middle.
Since this is a well-established result, this is a community wiki post.
Relevant question: Deciding whether $2^{\sqrt2}$ is irrational/transcendental
Kuzmin proved the following claim in 1930:
Theorem: If $\alpha\neq 0,1$ is algebraic, $\beta$ is positive and rational, not a perfect square, then $\alpha^{\sqrt{\beta}}$ is transcendental.
Unfortunately the paper is in Russian and I failed to find an English translation. A corollary of this is that $2^{\sqrt{2}}$ is transcendental, and so is its square root $\sqrt{2}^{\sqrt{2}}$.
The outlines of both Gelfond and Kuzmin's constructive proof can be found here.
As David Mitra pointed out the comments, Niven's book had a section dedicated to this. I love Niven's book so much. The technique is similar to the adapted proof I posted here, proof by contradiction.
Rough idea about the construction: First assuming $\alpha^{\sqrt{\beta}}$ is algebraic. Then using sufficient large degree Lagrange interpolation polynomial to approximate $e^{(\ln \alpha)x}$ at points $\{a+ b\sqrt{2}\}$ for $a,b\in \mathbb{Z}$. Let the number of points go to infinity the error will go to zero, this shows a transcendental function $\alpha^x$ can be interpolate using countably many algebraic points. Contradiction.
I don't think that you can actually prove Cauchy-Schwartz (CS) for an arbitrary inner product space (constructively). In Constructive Analysis by Bishop & Bridges they define inner product spaces so that CS holds:
However, for the special case of $\mathbb{R}^n$ it is possible to give a constructive proof, which can be found on page 83 of Constructive Analysis:
Best Answer
I. Constructions of the reals
Before we tackle the irrationality of $\log_2 3$, we need to briefly discuss how real numbers work in constructive mathematics.
In classical real analysis, we identify the real numbers with the Dedekind-complete ordered field. This does not work in constructive mathematics, since it requires Excluded Middle to show that the usual constructions of the set $\mathbb{R}$ satisfy Dedekind-completeness.
In fact, you cannot prove the existence of any Dedekind-complete ordered field in a constructive way. Assuming the existence of such a field implies the Limited Principle of Omniscience, a well-known non-constructive principle.
Instead, the real numbers are usually presented either as equivalence classes of exponentially fast-converging Cauchy sequences, or as two-sided Dedekind cuts. You cannot constructively prove that these constructions yield Dedekind-complete ordered fields. You can't even prove that the two presentations define the same set! Because of this, people sometimes refer to the two sets as the "set of Cauchy reals" and the "set of Dedekind reals" respectively.
In what follows, I will sketch a proof of existence of $\log_2 3$ that works for both the Cauchy reals and the Dedekind reals. I will then show that it's irrational.
II. Construction of $\log_2 3$
Consider the exponential function $f(x) = 2^x$.
One can define this easily for whatever construction of the reals you have in mind (Dedekind or Cauchy). You seemingly already accept that exponential functions can be defined, and that $f$ is continuous on the closed interval $[1,2]$. In any case, I won't prove this here, since the usual real-analytic proofs happen to work.
I will, however, point out that $f$ is monotone on this interval: you should show that it satisfies the inequality $$\frac{1}{2}(y - x) \leq 2^y - 2^x$$ for every $1 \leq x \leq y \leq 2$.
I will now define a number $r$ such that $f(r) = 3$ by bounding $r$ from above and below using two sequences of rational numbers $a: \mathbb{N} \rightarrow \mathbb{Q}$ and $b: \mathbb{N} \rightarrow \mathbb{Q}$. I will first give an explicit algorithm defining these two sequences, so you'll know that they are defined in a constructively acceptable way. Then, I will prove that these sequences converge together exponentially fast, so they define a real number. I then prove that the value they converge to, which I denote $r$, satisfies $2^r = 3$. Finally, I will give a constructive proof showing that $r$ is not rational.
II.1. The algorithm
We define the two sequences by recursion on their argument $n \in \mathbb{N}$. For the base case $n = 0$, we have $b_0 = 0$ and $a_0 = 1$.
For $n=k+1$, we start by recursively computing $b_k$ and $a_k$, and then do as follows:
II.2. Fast convergence
Notice that $a_n - b_n \leq \frac{2}{2^n}$ holds for all $n$. Since the sequences were defined by recursion, we can prove this by induction.
In the base case $a_0 - b_0 = 2 - 1 = 1 = \frac{2}{2}$.
In the inductive case, we know that $a_n - b_n \leq \frac{2}{2^n}$, and we seek to establish that $a_{n+1} - b_{n+1} \leq \frac{1}{2^n}$. There are three cases to check, depending on whether we finished in case 1, case 2 or case 3 in the computation of $a_{n+1},b_{n+1}$ above. In the first case, $a_{n+1} - b_{n+1} = a_n - m_n$. In the second, $a_{n+1} - b_{n+1} = m_n - b_n$. In the third, $a_{n+1} - b_{n+1} = u_n - \ell_n$. In each case, it's clear that $a_{n+1} - b_{n+1} = \frac{1}{2}(a_n - b_n) \leq \frac{1}{2} \frac{2}{2^n} = \frac{1}{2^n}$. This concludes our proof.
Since $a_n - b_n = \frac{2}{2^n}$ and $a_n > b_n$ always holds, we can turn the two sequences into an exponentially fast-converging Cauchy sequence, or use them to define a two-sided Dedekind cut. Either way, we get a constructive real number, which we'll denote $r$.
II.3. Logarithm of three
I claim that $f(r) = 2^r = 3$.
Since $f$ satisfies continuity and preserves order, it's sufficient to show that $f(a_n)$ and $f(b_n)$ both converge to 3. Again, we'll do induction on $n$.
In the base case, since $f$ is monotone on $[1,2]$, we have $f(b_0) = f(1) = 2 \leq 3 \leq 4 = f(2) = f(a_0)$.
In the inductive case, assume we have $f(b_n) \leq 3 \leq f(a_n)$. We need to show that $f(b_{n+1}) \leq 3 \leq f(a_{n+1})$ holds as well.
As in our previous proof, we have 3 cases to consider, depending on whether our computation ended in cases 1,2 or 3. Cases 1 and 2 are similar, so I'll just do case 1.
In case 1, $a_{n+1} = a_n$ and $b_{n+1} = m_n$ so all we need to show is that $f(m_n) \leq 3 \leq f(a_n)$. We know $3 \leq f(a_n)$ by assumption, so that leaves $f(m_n) \leq 3$. But we actually know that $f(m_n) \leq j_n < 3$, so we're done.
That leaves case 3. Here we know that $a_{n+1} = u_n$ and $b_{n+1} = \ell_n$, so we must show $f(\ell_n) \leq 3 \leq f(u_n)$. Recall that we chose $i_n$ and $j_n$ so that $i_n \leq 3 \leq j_n$ (otherwise, we would have ended up in case 1 or case 2). Consequently, it suffices to show that $f(\ell_n) \leq i_n$ and $j_n \leq f(\ell_n)$.
This is where we'll use the bound on $f$ that I stated in the beginning.
We have $f(\ell_n) < i_n$ because $$f(m_n) - f(\ell_n) \geq \frac{1}{4}(m_n - \ell_n) = \frac{1}{8}(a_n-b_n)$$ so $f(\ell_n) \leq f(m_n) - \frac{1}{8}(a_n-b_n)$. But we choose $i_n$ so that $f(m_n) - \frac{1}{16}(a_n-b_n) < i_n$, so this means $f(\ell_n) < i_n$.
By identical reasoning, we have $f(u_n) > j_n$, since $f(u_n) - f(m_n) \geq \frac{1}{4}(u_n - m_n) = \frac{1}{8}(a_n-b_n)$, so $f(u_n)> f(m_n) + \frac{1}{8}(a_n-b_n) > j_n$.
This concludes our proof by induction that $f(a_n) \geq 3 \geq f(b_n)$.
Since $f$ is monotone and continuous, we know that $f(a)$ and $f(b)$ must converge to the same value $f(r)$, and we have just shown that the value must be $3$.
II.4. Irrationality
So there is a real number $r$ such that $2^r = 3$.
This number is not rational. Assume for a contradiction (Is this allowed? Yes!) that it was rational. We could then write $r = \frac{p}{q}$, and get that $2^\frac{p}{q} = 3$, and therefore $2^p = 3^q$. But the left hand side is not divisible by $3$, while the right hand side is, a contradiction. This suffices to prove that $r$ is irrational.
With a bit more work, you can prove a constructively stronger property as well: you can explicit bound the distance between $r$ and any rational number. I'll leave this as an exercise for the reader: the idea is to notice that if $2^p \neq 3^q$, you must also have $|2^p - 3^q| > 1$. Using this as a starting point, you can bound $\left|2^r - 2^{\frac{p}{q}}\right|$, and use an inequality like the one above to bound $\left|r - \frac{p}{q}\right|$.
III. Discussion
Is this any harder than the same proofs in classical analysis? Not really. By the time you know that exponential functions $x^y$ exist, you have all the tools to make the proof work, in either the classical or the constructive case. Depending on how your favorite development of analysis goes, you might even have logarithms before exponentials, since logarithms can arise as integrals of rational functions.
The algorithm computing $\log_2 3$ that I gave above is a standard one used for computing logarithms in (classical or constructive) exact real computation. It is in fact a bisection algorithm, similar to, but numerically more well-behaved than, the bisection method you use in a non-constructive real analysis course when you prove the Intermediate Value Theorem.
Now, you may have heard that the bisection proof of the IVT fails in constructive mathematics, since you cannot test whether the midpoint $f(m_n)$ satisfies $f(m_n) = 0$, $f(m_n) > 0$ or $f(m_n) < 0$. And what you heard is true: in general, the idea behind the IVT fails. But that doesn't mean that no function satisfies the IVT, only that you can't prove that all functions satisfy the IVT.
In fact, you can prove constructively that in particular $f(x) = 2^x$ satisfies the Intermediate Value Theorem, so every positive number, even if it is irrational, has a base-2 logarithm. The proof is a bisection argument that makes heavy use of the essential fact that $2^x$ is monotone. It is much more complicated than the algorithm for finding $\log_2 3$ that I outline above, since my algorithm makes essential use of the fact that $3$ is a rational number, and hence can be compared using $<,=,>$ to other rational numbers.