Is there an intuitionist (i.e., constructive) proof of the infinitude of primes?

Due to a widely propagated historical error, it is commonly misbelieved that Euclid's proof was by contradiction. This is false. Euclid's proof was in fact presented in the obvious constructive fashion. See Hardy and Woodgold's Intelligencer article [1] for a detailed analysis of the history (based in part on many sci.math discussions [2]).

The key idea is not that Euclid's sequence $\ f_1 = 2,\ \ \color{#0a0}{f_{n}} = \,\color{#a5f}{\bf 1}\, +\, f_1\cdot\cdot\cdot\cdot\, f_{n-1}$ is an infinite sequence of primes but, rather, that it's an infinite sequence of coprimes, i.e. $\,{\rm gcd}(f_k,f_n) = 1\,$ if $\,k<n,\,$ since then any common divisor of $\,\color{#c00}{f_k},\color{#0a0}{f_n}\,$ must also divide $\, \color{#a5f}{\bf 1} = \color{#0a0}{f_n} - f_1\cdot\cdot\, \color{#c00}{f_k}\cdot\cdot\, f_{n-1}.$

Any infinite sequence of pairwise coprime $\,f_n > 1 \,$ yields an infinite sequence of distinct primes $\, p_n $ obtained by choosing $\,p_n$ to be any prime factor of $\,f_n,\,$ e.g. its least factor $> 1$.

A variant that deserves to be much better known is the following folklore one-line proof that there are infinitely many prime integers

$$n\:\! (n+1)\,\ \text{has a larger set of prime factors than does }\, n\qquad$$

because $\,n+1>1\,$ is coprime to $\,n\,$ so it has a prime factor which does not divide $\,n.\,$ Curiously, Ribenboim believes this proof to be of recent vintage, attributing it to Filip Saidak. But I recall seeing variants published long ago. Does anyone know its history?

For even further variety, here is a version of Euclid's proof reformulated into infinite descent form. If there are only finitely many primes, then given any prime $\,p\,$ there exists a smaller prime, namely the least factor $> 1\,$ of $\, 1 + $ product of all primes $\ge p\:.$

It deserves to be much better known that Euclid's constructive proof generalizes very widely - to any fewunit ring, i.e. any ring having fewer units than elements - see my proof here. $ $ The key idea is that Euclid's construction of a new prime generalizes from elements to ideals, i.e. given some maximal ideals $\rm\, P_1,\ldots,P_k,\, $ a simple pigeonhole argument employing CRT deduces that $\rm\, 1+P_1\:\cdots\:P_k\, $ contains a nonunit, which lies in some maximal ideal which, by construction, is comaximal (so distinct) from the initial max ideals $\rm\,P_1,\ldots,P_k.$

[1] Michael Hardy; Catherine Woodgold. Prime Simplicity.
The Mathematical Intelligencer, Volume 31, Number 4, 44-52 (2009).

[2] Note: Although the article [1] makes no mention of such, it appears to have strong roots in frequent sci.math discussions - in which the first author briefly participated. A Google groups search in the usenet newsgroup sci.math for "Euclid plutonium" will turn up many long discussions on various misinterpretations of Euclid's proof.

Your question is predicated on a common misconception. In fact Euclid's proof is thoroughly constructive: it gives an algorithm which, upon being given as input any finite set of prime numbers, outputs a prime number which is not in the set.

Added: For a bit more on mathematical issues related to the above algorithm, see Problem 6 here. (This is one of the more interesting problems on the first problem set of an advanced undergraduate number theory course that I teach from time to time.)

Euclid's theorem is intuitionistic. Given any finite set S of primes, their product plus one is not divisible by any of the primes and hence is divisible by some prime not in S. This gives a concrete upper bound on the n-th prime as well -- though of course it's astronomical.