The Green-Tao primes theorem "The primes contain arbitrarily long arithmetic progressions" Ann Math 2008, is certainly a tour de force and extremely technical.
The authors point out that they have taken precautions to not use Axiom of Choice. Choice is mentioned several times in the paper, eg p.485:
In particular we shall always remain in the ﬁnitary setting of ZN , in contrast to the standard ergodic theory framework in which one takes weak limits (invoking the axiom of choice) to pass to an inﬁnite measure-preserving system.
In the original ergodic theory arguments of Furstenberg this algorithm was not guaranteed to terminate, and indeed one required the axiom of choice (in the guise of Zorn’s lemma) in order to conclude the structure theorem. However, in our setting we can terminate in a bounded number of steps...
In terms of constructive vs classical mathematics however AC is only one of the forbidden axioms. Another is excluded middle. But I can't follow the paper to understand whether results that invoke excluded middle are used.
Kolmogorov, in "On the tertium non datur principle" writes "a proposition is pseudo-true if its double negation is true".
Is the Green-Tao theorem true or pseudo-true?