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(joint work with Peter Schuster):
- Maximal ideals in countable rings, constructively, In Revolutions and Revelations in Computability: 18th Conference on Computability in Europe, CiE 2022, Swansea, UK, July 11–15, 2022, Proceedings. https://doi.org/10.1007/978-3-031-08740-0_3 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.
