Is there an intuitionist (i.e., constructive) proof of the infinitude of primes? This question relates to a discussion on another message board. Euclid's proof of the infinitude of primes is an indirect proof (a.k.a. proof by contradiction, reductio ad absurdum, modus tollens). My understanding is that Intuitionists reject such proofs because they rely on the Law of the Excluded Middle, which they don't accept. Does there exist a direct and constructive proof of the infinitude of primes?
 A: Here's a simple direct proof that not only shows there is an infinite number of primes, but gives a lower bound on how many primes are less than $N$. The idea comes from Erdős.
Let $\pi(N)$ be the number of primes $\leq N$ for a positive integer N. Any positive integer $\leq N$ can be written in the form $$B^2{p_1}^{e_1} {p_2}^{e_2} ... {p_{\pi(N)}}^{e_{\pi(N)}}$$ where the $e_i$'s are 0 or 1 and $B\leq \sqrt N$.
There are at most $2^{\pi(N)}\sqrt N$ possible numbers of this form, and so we have $$2^{\pi(N)}\sqrt{N}\geq N$$ which gives us $$\pi(N)\geq {\log{N}\over{2 \log 2}}$$ which is clearly unbounded.
This idea is used in Erdos' nice proof that $\sum {1\over p}$ diverges, although that is a proof by contradiction and so would not satisfy the intuitionist school. It goes like this. Assume the sum converges. Then there is some $k$ such that ${\sum_{i \geq k+1}} {1\over p_i} < 1/2$. Call the primes $\leq p_k$ the "small" primes, and the primes $\geq p_{k+1}$ the "big" primes. We can divide the positive integers $\leq N$, for arbitrary N, into two groups: those that are divisible by a "big" prime, and those that are not. An upper limit on the number divisible by a "big" prime is $N/2$ (this comes from the assumption that the sum of the reciprocals of the big primes is $\leq 1/2$), and an upper limit on the number not divisible by a "big" prime is $2^k\sqrt N$. Since those two categories include all the positive integers $\leq N$, we must have $N/2+2^k \sqrt N \geq N$. However, that is not true for sufficiently large $N$, and so we have our contradiction, and the series diverges. 
A: 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 explained below. 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.
A: 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.)
A: 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.
A: Although this is an old post it is instructive to cite the following study on constructive mathematics which clears some common misconceptions related to constructive mathematics by people trained exclusively in classical mathematics.
For example the difference between proof by negation (valid in constructive mathematics) vs proof by contradiction (not valid in constructive mathematics in general)
FIVE STAGES OF ACCEPTING CONSTRUCTIVE MATHEMATICS (ANDREJ BAUER)

Abstract. On the odd day, a mathematician might wonder what
constructive mathematics is all about. They may have heard arguments
in favor of constructivism but are not at all convinced by them, and in
any case they may care little about philosophy. A typical introductory
text about constructivism spends a great deal of time explaining the
principles and contains only trivial mathematics, while advanced
constructive texts are impenetrable, like all unfamiliar mathematics.
How then can a mathematician find out what constructive mathematics
feels like? What new and relevant ideas does constructive mathematics
have to offer, if any? I shall attempt to answer these questions.

There in you can find explanations why Euclid's proof is valid in constructive mathematics as it is proof by negation.
