In my answer explaining the differences between Lean and Coq, I emphasized that Lean is "essentially classical" mostly due to sociological norms. Nonetheless, even after posting that, I questioned it myself a bit. There was some push-back by François G. Dorais explaining that he regularly uses Lean for constructive mathematics. And I don't think he is the only one.
I think there are a few things which are clear:
mathliblibrary is by design fully classical. This isn't a strange decision in that most non-DTT proof assistant libraries like metamath/set.mm, Mizar/MML, Isabelle/HOL/AFP, and HOL-Light all (to my understanding) have the same classical centric design principle. But it does mean that if one wants to do constructive mathematics in Lean, one would likely need to avoid
- Lean without any extra axioms is constructive, for some definition of constructive. I believe, but maybe I'm mistaken, that Lean without axioms is basically propositionally equivalent to Coq with the axiom of unique identity proofs (UIP) (ignoring maybe differences in how they handle universes and a few other minor things). Since Lean has UIP it can't directly handle HoTT (at least not without the tricks used in the Lean 3 HoTT Library), but that it should be otherwise very similar to base Coq (with UIP). Also Lean and Coq have different definitional/computational properties (namely Lean's subsingleton elimination + proof irrelevance can break transitivity of definitional equality and therefore break subject reduction), which I know some constructivists might not consider ideal.
How usable is the Lean standard library (in Lean 3 or Lean 4) for doing non-HoTT constructive mathematics?
Even if one could in theory do constructive mathematics in Lean with the core theory, I wonder how much the standard library supports this or gets in the way. For example, does the user have to constantly worry about LEM being introduced via various forms of automation---like the equation compiler,
rfl (definitional equality), common built-in tactics (
rw, etc.)? Does the user have to avoid many of the definitions in the standard library (since maybe they are not constructive)? Does the user have an ergonomic way to guarantee that their proofs don't use LEM or AC, other than manually checking the axioms for each proof? In general, is it feasible to build a library of constructive mathematics in Lean (separate from
mathlib of course), or would that be painful and antithetical to the Lean standard library design?
Note, I'm not taking a position if Lean needs to support constructive reasoning at any level, I'm just curious how feasible it is to do. I feel like I've heard mixed messages on this topic.