Intuitionistic logic and explicit existence proofs I have read that to intuitionistically prove a statement of the form $\exists x.\varphi,$ we have to actually describe such an $x$ as an explicit expression (with free variables from $\varphi$, excepting $x$). Is this just a fluffy heuristic, or can we actually formalize and prove this claim?

One of the characteristics of many constructive theories is that they have the "term existence property": if a statement $(\exists x)\phi(x)$ is provable, then there is a term $t$ such that $\phi(t)$ is provable. Moreover, usually $t$ can be extracted algorithmically from a formal proof of $(\exists x)\phi(x)$.

The term existence property is exactly a rigorous way to say that, if an existential statement is provable, then it is possible to explicitly describe a witness. Many constructive theories have this property or restricted version of it. The restriction to the case where the $(\exists x)$ quantifies over natural numbers is usually of particular interest.

The current version of the wikipedia article has some useful information and references.