There does not exist an even prime greater than two: is there an intuitionistic proof? My own feeble understanding of intuitionism is that it is constructive and that, by not accepting the law of excluded middle, proofs by contradiction are eschewed.
For my background on the topic, see this question.
I'm curious: how does intuitionism handle the following?

Theorem: There does not exist an even prime greater than two.
Proof: Suppose $p>2$ is such a prime. Then, by definition of what it means to be even, $p=2k$ for some $k\in \Bbb Z$, meaning $k\mid p$. Now $2k>2$, so $k>1$. But $k\neq p$ since otherwise $p=2p$ implies $1=2$, a contradiction. $\square$

Perhaps I just lack the imagination necessary for a constructive proof.
Please help  :)
 A: There's no intuitionism/constructivism issue going on here at all.

First of all, as a general matter of practice you need to keep separate the notions of proof by contradiction and proof by negation. The latter is intuitionistically acceptable!
Specifically, let's say we interpret "$\neg p$" as shorthand for "$p\rightarrow\perp$" (this is pretty standard) and accept the inference rule $$(\mathsf{ded})\quad{A,p\vdash q\over A\vdash p\rightarrow q}$$ (= the deduction theorem) while rejecting double negation elimination. Then the proof by negation inference rule $$(\mathsf{nega})\quad{A,p\vdash\perp\over A\vdash\neg p}$$ is justifiable: from $A,p\vdash\perp$ we get $A\vdash p\rightarrow\perp$, which literally is the sequent $A\vdash\neg p$.
If we replace "$p$" by "$\neg p$" in the above we get $${A,\neg p\vdash \perp\over A\vdash\neg\neg p}$$ but the bottom sequent is not the same as $A\vdash p$ since we've rejected double negation elimination! Consequently the proof by contradiction inference rule $$(\mathsf{contra})\quad{A,\neg p\vdash \perp\over A\vdash p}$$ is not justified by our logical hypotheses so far.

This is all to say that a lot of the "elementary" examples of proof by contradiction are actually completely fine intuitionistically, since they're not proof by contradiction at all. Of course this is a distinction which doesn't exist classically, so is easy to miss at first.
But this is in fact only part of the story! We also need, when thinking nonclassically, to be more careful how we even phrase our goal. For example, consider the following statement:

If $x$ is an even number bigger than $2$, then $x$ has a factor strictly between $1$ and $x$.

There are no negations involved here whatsoever, and the obvious argument "$2$ divides $x$ and is strictly between $1$ and $x$" (once we've written out what "even" means) goes through perfectly. Things only become "negation-flavored" when we introduce unnecessary negations, a la "$\neg$ (there is an even number $x>2$ such that $\neg$ ($x$ is prime))." But the fact that we are allowed proof by negation means that such negation-introduction preserves intuitionistic provability.
As a toy example of this, consider the following proof that the sequent $$p\vdash\neg\neg p$$ is intuitionistically valid (unlike $\neg\neg p\vdash p$).

*

*First, by modus ponens we have $p, \color{red}{p\rightarrow\perp}\vdash \perp.$


*By $(\mathsf{ded})$ we have $p\vdash \color{red}{(p\rightarrow\perp)}\rightarrow\perp$.


*But using our definition of $\neg$, this is literally the same sequent as $p\vdash \neg\neg p$.
A good exercise at this point is to intuitionistically prove triple negation elimination $$\neg\neg\neg p\dashv\vdash\neg p.$$
