The nlab claims that the maximal ideal theorem in Heyting Algebras (i.e. for every proper ideal in a Heyting Algebra, there is a maximal ideal that contains it) implies the axiom of choice. Sadly, it does not cite any proofs and I've been unable to prove this, I'd appreciate any proofs/references.
I find this particularly interesting as it's known that the maximal ideal theorem for Boolean Algebras is strictly weaker than the axiom of choice. Yet, the same theorem applied to the apparently slightly bigger class of Heyting Algebras suffices to prove choice.
Here is a full proof of AC from the Maximal Ideal Principle in Heyting algebras.
So suppose $(X_i)_{i\in I}$ is a family of infinite nonempty pairwise disjoint sets. We want to find a choice function for this family. Consider the topological space $F$ with points all nontrivial (possibly partial) choice functions for $(X_i)_{i\in I}$, that is functions $f$ with domain $\emptyset\neq\mathrm{dom}(f)\subseteq I$ with $f(i)\in X_i$ for all $i\in \mathrm{dom}(f)$. The topology is generated by the open basis sets of the following form: If $s$ is a finite function with $\mathrm{dom}(s)\subseteq I$ and $s(i)\subseteq X_i$ cofinite for all $i\in \mathrm{dom}(s)$ then $$U_s=\{f\in F\mid f(i)\in s(i)\text{ for all }i\in\mathrm{dom}(s)\cap \mathrm{dom(f)}\}$$ is basic open. It is easy to check that these sets indeed form a basis of a topology.
First note that $F$ is compact. If $\mathcal U$ is an open cover of $F$ then first of all we can assume all elements of $\mathcal U$ to be basic open sets. Now it is straightforward to build a first order theory $T$, any model of which would yield some $f\in F\setminus\bigcup \mathcal U$. Use constants $c_i$ and $\dot x$ for $i\in I$ and $x\in X_i$. For each $U_s\in\mathcal U$, our theory contains the disjunction over $c_i=\dot x$ for $i\in \mathrm{dom}(s)$ and $x\in X_i\setminus s(i)$ (note that this is a finite disjunction). As $\mathcal U$ is an open cover, this theory does not have a model. Our assumption clearly implies the Boolean Prime Ideal Theorem and hence Gödel's completeness theorem holds. It follows that $T$ is inconsistent, so there is a finite $T_0\subseteq T$ which is inconsistent. The corresponding finite subset of $\mathcal U$ is thus a finite open subcover.
The Heyting algebra we are now going to look at is the collection of open sets in $F$. There is a natural way to to define implication and note that disjunction and conjunction are given by union and intersection. So let $\mathcal I$ be a maximal ideal on $H$ as guaranteed by our assumption.
Proof: Let $i\in I$ and let $x\in X_i$. If $U_{i\mapsto X_i\setminus\{x\}}\in\mathcal I$, we are done, so assume this is not the case. The ideal $\mathcal I$ cannot be enlarged to a proper ideal by adding $U_{i\mapsto X_i\setminus\{x\}}$ and hence there is some $O\in\mathcal I$ with $O\cup U_{i\mapsto X_i\setminus\{x\}}=F$. By compactness, there are $s_0,\dots, s_n$ so that $U_{s_0}, \dots ,U_{s_n}\subseteq O$ and $$U_{s_0}\cup\dots\cup U_{s_n}\cup U_{i\mapsto X_i\setminus \{x\}}=F.$$ Clearly, each $U_{s_k}$ is in $\mathcal I$. Next, note that each $U_{s_k}$ is a finite intersection of sets of the form $U_{j\mapsto X_j\setminus\{y\}}$ for some $j\in I$ and $y\in X_j$. As any maximal ideal is a prime ideal, we can find for each $k\leq n$ some $j_k$ and $x_k\in X_{j_k}$ so that $U_{s_k}\subseteq U_{j_k\mapsto X_{j_k}\setminus \{x_k\}}=: U_k$ with $U_k\in \mathcal I$. Hence $$U_0\cup\dots\cup U_n\cup U_{i\mapsto X_i\setminus \{x\}}=F.$$ We will assume all $U_0,\dots, U_n$ to be different, otherwise shrink the list. Now if all $j_0,\dots, j_n, i$ were different, then the partial choice function which maps $j_k$ to $x_k$ and $i$ to $x$ would not be covered, contradiction. So there msut be a repetition. But we cannot have $j_k=j_l$ for $l\neq k\leq n$ as then $U_k\cup U_l=F$ (since then $x_k\neq x_l$), which is impossible as $\mathcal I$ is a proper ideal. Hence there is $k\leq n$ with $j_k=i$ and it follows that $U_{i\mapsto X_i\setminus\{x_k\}}\in\mathcal I$ witnesses the claim.$\square$
Finally, observe that for $i\in I$, the $x\in X_i$ with $U_{i\mapsto X_i\setminus\{x\}}$ is unique! Otherwise, as before, there would be two sets in $\mathcal I$ which cover the whole of $F$. This readily gives us the desired choice function.