How to construct a constructive proof from a non-constructive proof using prime ideals?

Exactly what kind of answer you get depends on the kind of proof you start with and what exactly you mean by constructive. But the proof mining approach offers an answer to some questions of this kind.

The crucial idea that comes out of it is that, to prove concrete facts, one can generally replace the notion of a prime ideal with sort of "local primality" notion. Basically, if P is a possibly prime ideal, one often doesn't need it to be truly prime to complete the proof; it might suffice, say, to look at a single pair $f_Pg_P\in P$ and need $f_P\in P$ or $g_P\in P$ to complete the argument. Therefore one can first fix the function $P\mapsto (f_P,g_P)$, and then ask for an ideal P with the property that $f_P\in P$ or $g_P\in P$. (More generally, we might hope to look at only finitely many test cases of this kind.)

At least in suitably restricted settings (say, where we are considering ideals which have reasonable finitary representations of some kind), one can extract constructive proofs along these lines.

Under suitable circumstances (in particular, one has to consider questions about how the ideal $P$ is represented) one can obtain constructive proofs this way. William Simmons I will be soon (I hope by the end of the month) uploading a paper on proof mining in polynomial and differential polynomial rings which tackles some related problems. Being polynomial rings, however, makes a big difference, because it means ideals are guaranteed to have finite representations.

Here is a method which is very efficient in the case were "constructive" is interpreted as "no axiom of choice at all, not even countable and no law of excluded middle", i.e. essentially "topos logic".

It is possible to construct a very well behaved "Zariski spectrum" (including its structural sheaf whose globale section will be $A$ exactly) as a locale instead of a topological space: on will simply say that $\text{Spec } A$ is the classifying space of the theory of "complement of prime ideals" described below.

One can then construct the structural sheaf and so one and it is relatively trivial that the set of global section is $A$ and that an element of $A$ which is nowhere invertible in the structural sheaf is nilpotent.

points of the spectrum are still the prime ideal, but because it is now a locale instead of a topological space one does not really care about existence of points or not.

well this is not entirely true: technically the point (in the sense of classyfing topos) are the "complement of prime ideal" I.e. subset $I$ that satisfies $0 \notin I$, $1 \in I$, if $x+y \in I$ then $x\in I$ or $y \in I$ and $yx \in I$ if and only if $x \in I$ and $y \in I$. assuming the law of excluded middle this is the same as saying that the complement of $I$ is a prime ideal...

almost all "geometrical argument" can be made constructive by replacing the ordinary zariski spectrum by the localic Zariski spectrum, and this include most prof that involve using all prime ideal.

This technique is very well known among topos theorist but I don't know any reference explaining this clearly, maybe someone will know of one ?

In the mean time, I will try to give a little more explanation: Basically, instead of saying "let $\rho$ be a prime ideal" you move to the structural sheaf over the Zariski spectrum, especially if you know a little bit of internal logic this amount to assume that you have a subset $I$ as above which play the role of (the complement of) your prime ideal and if you can prove that your element $x$ is never in $I$ then it is nilpotent or if your some ideal "always contains an element of $I$" it has to be the whole ring and so one... Moreover, the structural sheaf is the localization at $I$ and $I$ is exactly the set of element that are invertible in the structural sheaf.

The drawback is that the rest of the proof has to be performed internally in in the topos of sheaves over the zariski spectrum, hence really has to be constructive (not involving the law of excluded middle) or has to involve working explicitly with sheaves.

Let me illustrate this on your two examples:

The sum of two nilpotent is nilpotent:

($I$ denote the universal "completment of prime ideal" in the logic of $spec A$, it is also the subobject of the structural sheaf of invertible element)

let $x$ and $y$ be nilpotent, internally in $\text{Spec } A$ $x$ and $y$ are not invertible (i.e. not element of $I$) hence $x+y$ is not invertible either (because $x+Y \in I \Rightarrow x \in I$ or $y \in Y$), hence $x+y$ is nowhere invertible on the spectrum hence nilpotent.

The thing about sum of ideals: well the exact same proof apply, just redefine $V(A)$ to be the corresponding closed subspace of the Zariski spectrum instead of a set of prime ideal...

Since this is somewhat hidden in the comments, let me give the following answer:

• The statement that the sum of two nilpotents is nilpotent is so basic that it seems to be used in the construction and the verification of the Zariski locale/topos/lattice. I don't think that constructive algebra can prove this without circular arguments.
• However, the statement $I+J=A \Rightarrow I^n+J^m=A$ can be proven by working in the lattice of radical ideals: $$\sqrt{I^n+J^m}=\sqrt{I^n} \vee \sqrt{J^m}=\sqrt{I} \vee \sqrt{J}=\sqrt{I+J}=A.$$ Whenever one uses the open subset $D(I)$ in a proof, one may simply replace it by the radical ideal $\sqrt{I}$