I would like to solve the beginner's standard exercise which claims that a point of $\mathrm{Spec} \ R$ is closed iff it is a maximal ideal.
The reverse implication is easy. The direct one seems much subtler. If $P = V(I)$ then, since there exist a maximal ideal $M$ containing $P$, it would follow that $\{P, M\} \subseteq V(I) = P$, whence $P=M$. In order to show the existence of $M$ I applied Zorn's lemma to the set of ideals containing $P$.
The question is the following: is there any other proof of the above implication that does not (indirectly) use the axiom of choice? My concern is that I may be using a cannon to shoot a fly. Also, it would be the first time that I see closedness of points to require the axiom of choice. If the axiom is indeed needed in general, are there "nice" classes of rings for which we could get away without it?
The following example shows that the use of the axiom of choice cannot be avoided. Let $A$ be the ring of entire functions, and let $B$ be the localization of $A$ obtained by inverting $z-a$ for each $a\in\mathbb{C}$ (equivalently, let $B$ be the ring of meromorphic functions on $\mathbb{C}$ with only finitely many poles). The ring $A$ is a Bezout domain, and hence so is $B$. In particular, $0$ is a prime ideal of $B$.
Now suppose $P\subset B$ is a prime ideal with a nonzero element $f\in P$. Since $f$ is not a unit in $B$, it must have infinitely many zeroes. Let $Z$ be the set of zeroes of $f$. Since $Z$ is a closed discrete subset of $\mathbb{C}$, it is in bijection with $\mathbb{N}$ (exercise: you can prove this without choice). Now let $U$ be the set of subsets $S\subseteq Z$ such that there exists $g\in P$ whose vanishing set is $S$. Then $U$ must be an ultrafilter on $Z$ (the fact that $U$ is closed under binary intersections comes from the fact that $B$ is a Bezout domain and intersections of zero sets correspond to gcds of functions; the fact that if $S\cup T=Z$ then either $S\in U$ or $T\in U$ is because you can find a function $g$ vanishing on $S$ and a function $h$ vanishing on $T$ so that $gh$ is divisible by $f$, so by primeness either $g\in P$ or $h\in P$). Moreover, since any function with finitely many zeroes is a unit in $B$, $U$ must be nonprincipal.
Thus if there exists a nonzero prime ideal in $B$, there exists a nonprincipal ultrafilter on $\mathbb{N}$. Now work in a model of ZF where there exist no nonprincipal ultrafilters on $\mathbb{N}$. In this model, $0$ is the only prime of $B$, so $0$ is a closed point of $\operatorname{Spec} B$. However, $0$ is not a maximal ideal of $B$.