It's easier to think about the Intermediate Value Theorem, which is equivalent to the Brouwer Fixed-Point Theorem for the unit interval.

The main issue is that dichotomy for (Cauchy) real numbers is not constructively valid: given two real numbers $\alpha,\beta$, there is no algorithm to decide whether $\alpha \leq \beta$ or $\alpha \geq \beta$. This principle is equivalent to the Lesser Limited Principle of Omniscience (LLPO) and it's non-constructive nature is illustrated by a classic Brouwerian counterexample:

Define the sequence of rationals $(a_n)_{n=0}^\infty$ by $a_n = (-2)^{-k}$ if $k \leq n$ and the first occurrence of the sequence $736667843909774044615061702878$ in $\pi$ begins $k$-digits after the decimal point; if there is no such $k \leq n$, then $a_n = 0$. This is a well-defined Cauchy sequence (with a known rate of convergence) so the limit $\alpha = \lim_{n\to\infty} a_n$ is a well-defined real number. Is $\alpha \geq 0$ or $\alpha \leq 0$?

If the given sequence does occur in $\pi$, then we will eventually know that $\alpha > 0$ or $\alpha < 0$ and respond accordingly. However, if the given sequence does not occur in $\pi$, though both answers are valid in this case, neither answer can be proven correct without an infinite amount of information about the digits of $\pi$ (which the example assumes is not known at this time).

Returning to the Intermediate Value Theorem, consider the piecewise linear function $f:[-1,1]\to[-1,1]$ that interpolates the points $(-1,1),(-1/2,\alpha),(1/2,\alpha),(1,1)$. The Intermediate Value Theorem says that there is a number $r \in [-1,1]$ such that $f(r) = 0$. Note that $\alpha \geq 0$ iff $r \leq 1/2$ and $\alpha \leq 0$ iff $r \geq -1/2$. Now, determining whether $r \leq 1/2$ or $r \geq -1/2$ is easy: compute $r$ to enough accuracy to know that it lies within an open interval with length $1$ and rational endpoints; that interval cannot contain both $1/2$ and $-1/2$ and that is enough to know whether $r \leq 1/2$ or $r \geq -1/2$.

So, from the above, we see that if we had a constructive proof of the Intermediate Value Theorem, we would also have a constructive proof of dichotomy. Since there is no constructive proof of dichotomy, there cannot be a constructive proof of the Intermediate Value Theorem and, for the same reason, there cannot be a constructive proof of the Brouwer Fixed-Point Theorem.

The Brouwerian counterexample above might not be convincing since we (at least believe) that we know nontrivial information about $\pi$. Of course, the specific number $\pi$ is irrelevant; it's just the traditional choice for Brouwerian counterexamples. Here is a similar example that relies on the existence of inseparable pairs of computably enumerable sets.

Say a sequence $(q_n)_{n=0}^\infty$ of rational numbers is *rapidly Cauchy* if $|q_n - q_m| \leq 1/2^N$ for all $m,n > N$. (This is one of the typical definitions of Cauchy real numbers.) Suppose we did have an algorithm $M$ to decide whether the limit of a rapidly Cauchy sequence is nonnegative or nonpositive.

Now given an index $e$, define $(a_{e,n})_{n=0}^\infty$ to be $a_{e,n} = (-1)^m/2^s$ if the $e$-th Turing machine halts in exactly $s \leq n$ steps and outputs $m$, and set $a_{e,n} = 0$ if the $e$-th Turing machine does not halt in $n$ or fewer steps. Each of these sequences is an effectively computable rapidly Cauchy sequence. If I apply my proposed $M$ to the $e$-th sequence, I obtain a total computable function $s:\mathbb N \to \{0,1\}$ such that if $s(e) = 0$ then $\lim_{n\to\infty} a_{e,n} \leq 0$ and if $s(e) = 1$ then $\lim_{n \to \infty} a_{e,n} \geq 0$.

Note that $\lim_{n\to\infty} a_{e,n} > 0$ iff $e$ belongs to the set $A$ of all indices for Turing machines that halt with even output, and $\lim_{n \to\infty} a_{e,n} \lt 0$ iff $e$ belongs to the set $B$ of all indices for Turing machines that halt with odd output. The pair $A,B$ is one of the standard prototypical examples of an inseparable pair, so there is no computable set $C$ such that $A \subseteq C$ and $B \cap C = \varnothing$. However, the set $C = \{e : s(e) = 1\}$ does exactly that!

singlerigorous meaning to it, because things that classically would all be considered as the BFPT (eg "BFPT for Cauchy reals" and "BFPT for Dedekind reals") may not be constructively equivalent. But once a single statement (up to constructive equivalence) is chosen, then certainly its constructive probability is a rigorous question. $\endgroup$ – Peter LeFanu Lumsdaine Apr 13 '15 at 16:12