3 ms·

I was asking a less sophisticated question. I think the answer is "Lean is constructive if you use the base system without known non-constructive axioms".