Lean, for instance, is based on the calculus of inductive constructions: “importing” mathlib into ZFC (without just building a model of CIC within it) would be incredibly difficult.
I just want to mention that Lean’s mathlib focuses on classical rather than constructive mathematics, and accepts routinely the law of excluded middle in proofs.
It focuses on classical rather than constructive mathematics.
Yes, terms in Prop are routinely defined nonconstructively, but this is all happening within the context of a constructive (or at least very much not set-theoretic) metatheory. So for instance LEM gets derived from choice by Diaconescu’s theorem, types are conventionally supposed to be constructive, you sometimes have to care about definitional vs. propositional equality, etc.
I just want to mention that Lean’s mathlib focuses on classical rather than constructive mathematics, and accepts routinely the law of excluded middle in proofs.
It focuses on classical rather than constructive mathematics.
Yes, terms in
Propare routinely defined nonconstructively, but this is all happening within the context of a constructive (or at least very much not set-theoretic) metatheory. So for instance LEM gets derived from choice by Diaconescu’s theorem, types are conventionally supposed to be constructive, you sometimes have to care about definitional vs. propositional equality, etc.