[cvoss]

Yes, but for an even more immediate reason. The axiom of choice itself is a non-constructive axiom. It asserts the existence of the inhabitant of a certain type, without in any way furnishing the inhabitant.

But Lean sequesters off the classical logic stuff from the default environment. You have to explicitly bring in the non-constructive tools in order to access all this. So, actually, I would disagree with GP that Lean's type system includes a choice axiom.

[nrds]

Right, I was about to comment the same thing that "Lean" does not itself assume choice. Mathlib4 does, and Lean4 is designed so that all the built-in stuff is _consistent_ with choice. But you can do purely constructive mathematics in Lean and it's is even designed so that any non-propositions depending on choice have to be annotated "noncomputable", so the walled garden of choice is baked in at a language level. Even within "noncomputable" code, choice still shows up in the axiom list if used.