Number Theory in a Choice-less World

I was reading this article on the axiom of choice (AC) and it mentions that a growing number of people are moving into school of thought that considers AC unacceptable due to its lack of constructive proofs. A discussion with Mariano Suárez-Alvarez clarified that this rejection of AC only occurs when it makes sense.

This got me thinking. What are some examples of theorems in number theory that require the axiom of choice or its equivalents (ie Zorn's lemma) for its proof?

Note: Someone mentioned to me that Fermat's Last Theorem requires AC. Can someone verify this?

If we take a narrow enough view of number theory, AC can in principle be dispensed with. Take a sentence $\varphi$ of (first-order) Peano Arithmetic, and let $\varphi'$ be the usual translation of $\varphi$ into the language of set theory. If $\varphi'$ is provable in ZFC, then $\varphi'$ is provable in ZF.

There is a substantial extension of this result called the Shoenfield Absoluteness Theorem.

Remark: The result could be viewed as an argument for the acceptability of AC. For even if AC is as a matter of fact false, it cannot lead to false elementary assertions about the integers, unless ZF already does. Thus even if one has philosophical doubts about it, one can freely use it to prove number-theoretic assertions.

This really depends on "what is number theory" for you. If you only think of statements about natural numbers then I cannot, for the life of me, come up with a good example of the axiom of choice hiding inside.

Things like Wilson's theorem, or Euclid's proof of the infinitude of prime numbers require no choice at all. Recall that ZF proves the consistency of PA, so things which are provable directly from PA do not require the axiom of choice.

On the other hand, modern number theory is a lot more than that. It is a tangled web of algebra and analysis which goes on to use heavy machinery from modern mathematics. We talk about ideals, about algebraic closures, we talk about $p$-adic fields and we talk about representation theory.

Many of those require the axiom of choice, perhaps we can then limit the choice we use if we are interested in things which "live" inside or around $\mathbb C$, but we would still have to use some portion like dependent choice and ultrafilter lemma.

My experience, which is among the group of people who are working on automorphic forms, Galois representations, and their interrelations, is that no-one cares about whether or not AC is invoked. I think for some, this is simply because they genuinely don't care. For others (such as myself), it is because AC is a convenient tool for setting up certain frameworks, but they don't believe that it is truly necessary when applied to number theory. (For reasons somewhat related to Asaf Karagila's answer, I guess: there is a sense that all the rings/schemes/etc. that appear are of an essentially finitistic and constructive nature, and so one doesn't need choice to work with them --- although no-one can be bothered to actually build everything up constructively, so, as I said, AC is a convenient formal tool.)

On a somewhat related note: My sense is that most number theorists, at least in the areas I am familiar with, argue with second order logic on the integers, rather than just first order logic, i.e. they are happy to quanitfy over subsets of the naturals and so on. And they are really working with the actual natural numbers, not just an arbitrary system satisfying PA. So it's not immediately clear as to whether results (such as FLT) which are proved for the natural numbers are actually true for any model of PA. But, as with the use (or not) of AC, it can be hard to tell, because people aren't typically concerned with this issue, and so don't phrase their arguments (even to themselves) in such as way as to make it easily discernible what axiomatic framework they are working in. (I think many have the view that "God made integers ...".) One example of this is the question of determining exactly what axiom strength is really needed to prove FLT. As far as I know, this is not yet definitively resolved.