When can we prove constructively that a ring with unity has a maximal ideal? Many commutative algebra textbooks establish that every ideal of a ring is contained in a maximal ideal by appealing to Zorn's lemma, which I dislike on grounds of non-constructivity.  For Noetherian rings I'm told one can replace Zorn's lemma with countable choice, which is nice, but still not nice enough - I'd like to do without choice entirely.
So under what additional hypotheses on a ring $R$ can we exhibit one of its maximal ideals while staying in ZF?  (I'd appreciate both hypotheses on the structure of $R$ and hypotheses on what we're given in addition to $R$ itself, e.g. if $R$ is a finitely generated algebra over a field, an explicit choice of generators.)
Edit:  I guess it's also relevant to ask whether there are decidability issues here.  
 A: I suspect that the most general reasonable answer is a ring endowed with a constructive replacement for what the axiom of choice would have given you.
How do you show in practice that a ring is Noetherian?  Either explicitly or implicitly, you find an ordinal height for its ideals.  Once you do that, an ideal of least height is a maximal ideal.  This suffices to show fairly directly that any number field ring has a maximal ideal:  The norms of elements serve as a Noetherian height.
The Nullstellensatz implies that any finitely generated ring over a field is constructively Noetherian in this sense.
Any Euclidean domain is also constructively Noetherian, I think.  A Euclidean norm is an ordinal height, but not at first glance one with the property that $a|b$ implies that $h(a) \le h(b)$ (with equality only when $a$ and $b$ are associates).  However, you can make a new Euclidean height $h'(a)$ of $a$, defined as the minimum of $h(b)$ for all non-zero multiples $b$ of $a$.  I think that this gives you a Noetherian height.
I'm not sure that a principal ideal domain is by itself a constructive structure, but again, usually there is an argument based on ordinals that it is a PID.
A: If the ring is countable (or the image of a linear well-ordering), then no choice of any kind (not even countable choice) and in fact not even the law of excluded middle is required: There is an explicit construction, admissible by the standards of constructive mathematics.
This result is due to Krivine and was elucidated by Berardi and Valentini. See here for an introduction: https://arxiv.org/abs/2207.03873
In the general case, we can force the ring to become countable by passing to a suitable extension of the universe. In the extended universe, we can apply the Krivine construction again. From the point of view of the extended universe, we will have succeeded in constructing a maximal ideal. From the point of view of the base universe, we will only have constructed a suitable sheaf of ideals.
The base universe and the extended universe validate the same first-order statements. (Constructively, this is a nontrivial fact.) Hence, even though a maximal ideal itself might not constructively exist, its first-order consequences will hold constructively.
This phenomenon is briefly discussed in Section 4 of the linked paper.
A: Unlike full choice, you probably use countable choice all over the place without even recognizing it. Every time you do something iteratively and then take some sort of limit to your construction, you're using countable choice. In many cases, if you do very careful bookkeeping, you can eliminate it on a case by case basis. But you have to be very careful. Without countable choice, the countable union of countable sets isn't necessarily countable.
A: It seems to me like there are two points here. 
(1) A ring is called noetherian if any ascending chain of ideals terminates. I think all the standard facts about noetherian rings can be proved without choice: $\mathbb{Z}$ is noetherian; fields are noetherian; $A$ noetherian implies $A[x]$ noetherian; that quotients of noetherian rings are noetherian; localizations of noetherian rings are noetherian; completions of noetherian rings are noetherian.
That should take care of most the rings we need in algebraic geometry. 
However, I am worried about another issue:
(2) The usual proof that noetherian rings have maximal ideal goes as follows. Let $A$ be a ring without maximal ideals. Take the ideal $I_0 = \{ 0 \}$. Since it is not maximal, choose an ideal $I_1$ which contains it. Choose an ideal $I_2$ which contains $I_1$. Continue in this manner to produce a chain $I_0 \subsetneq I_1 \subsetneq I_2 \subsetneq \cdots$. This doesn't terminate, so $A$ is not noetherian.
This proof, of course, uses countable choice. My gut feeling is that this can be eliminated for the same sort of rings I address in (1). But does anyone know a reference for this?
A: You should take a look at Coquand and Lombardi's "A Logical Approach to Abstract Algebra". 
They observe that commutative rings have a purely equational description, and so there are very strong metatheorems that apply to this theory: Birkhoff's completeness theorem for equational logic, of course; and also Barr's theorem, which states that if a geometric sentences is a consequences of a geometric theories with classical logic plus choice, it's also intuitionistically valid. (And all equational theories are also geometric theories.) 
They strengthen Barr's theorem a bit, by characterizing the relevant intuitionistic proofs,  and then "de-Noetherian-ize" several basic theorems which are typically proved using maximal ideals. 
A: There are certain kinds of rings that came to my mind when I saw this question. $K[v]:=$ Coordinate ring of an affine variety $V$ over a field $K$ , and $C(X, F)$:= the ring of continuous $F$-valued ($F$ a topological field) functions on a compact space $X$. In both examples one can construct maximal ideals as zero sets of minimal closed subsets of certain topological space (In one case $V$ and in other case $X$).  So for $C(X, F)$ some max ideals correspond to points of $X$, and for $K[V]$ some max ideals correspond to points in $V$.  
Another way to think about the question is the following analogy to it.  Under what hypothesis can we exhibit a basis of a vector space without using any form of choice? here the clear answer should be finite dimensional spaces! This gives a clear picture about what rings $R$ we should consider, they are $R$'s that are Artinian rings. 
About decidability I'd say think about boolean rings. The category of Boolean rings is equivalent to the category of Boolean algebras. Under that equivalence one have a correspondence between ideals and filters that takes maximal ideals to ultrafilters. If I'm not mistaken the existence of ultrafilters is equivalent to some form of choice (see    http://www3.interscience.wiley.com/cgi-bin/fulltext/103520653/PDFSTART  ) 
so the same form of choice should be equivalent to the existence of maximal ideals.
A: Here is a type of example coming from Analytic Geometry (in the sense of the second "GA" in Serre's "GAGA").
Consider a domain $D$ in $\mathbb C$. Then every $\mathbb C$-algebra morphism (aka character) $\chi : \mathcal O (D) \to \mathbb C  $ is of the form $ev_d:f \to f(d)$ with $d=\chi (z) \in D$. This is completely elementary: just write $f(z)= f(d)+(z-d)g(z)$ and let $\chi$ act on both sides of the equality.[You have to convince yourself that $d$ is in $D$, not just in $\mathbb C$: else $1=(z-d).(z-d)^{-1}$ would lead to 1=0 by applying $\chi$].
[From this Lipman Bers proved in 1948 that, given two domains $D,D'\subset \mathbb C$, a purely algebraic isomorphism  $u:\mathcal O (D) \to\mathcal O (D')$ necessarily comes from an analytic isomorphism $f=u(z): D' \to D$.]
A vast generalization is that for any Stein manifold (or even Stein space) X, all characters $\mathcal O (X) \to \mathbb C $ are evaluations at a point of $X$, and yield maximal ideals $ker \chi$ of $X$.
This is proved in Grauert-Remmert's book "Theory of Stein spaces" and looking rather superficially at the proof I THINK the axiom of choice is not used.
This is certainly not a satisfactory answer to Qiaochu's question (in particular I know nothing of other maximal ideals in $\mathcal O (X)$: do such exist?)  but maybe these not so well-known results might interest some reader.
