How usable is Lean for constructive mathematics?

Question

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:

• Lean's mathlib library 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 mathlib.
• 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 (simp, 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.

Answer 1

First, a quick disclaimer: I am not a constructivist! However, I am a logician and I care about aspects of constructive mathematics and I really care about computability in general.

As Jason mentioned, I have used Lean for many years starting with Lean 2, often to formalize constructive mathematics. I never had major issues, so I can testify that it is indeed possible. As a proof-of-concept, I am opening the GitHub repository for the base part of my current Lean 4 library. (This is ahead of my plans, as you may notice by the general lack of documentation. There's a lot more where that came from but I don't plan on releasing more before this Summer.) You will notice that my library is very much constructive-aware.

To answer specific parts of the question: no parts of the standard Lean 2/3/4 library will surreptitiously introduce LEM or AC. It's true that the standard library contains these statements as axioms but they aren't used outside the Classical namespace. So ignoring that namespace takes care of much of these worries. One can always check that classical axioms are not used using the #print axioms command.

Whether Lean's type theory is constructively sound is debatable. Bishop would certainly criticize Lean's quotients. Martin-Löf might question the impredicativity of Prop. Singleton elimination and UIP are also sketchy. These are strongly built into the Lean core. On the other hand, these are also some of the main features that make Lean practical. I wouldn't want to give these up so I'm happy with Lean's "light" constructivism.

As I said before, I am not a constructivist. My main interest is in computable mathematics, while I am apprehensive of the noncomputable keyword, I am not at all allergic to classical reasoning. For certain tasks, I enjoy making Prop classical by using the axiom weakEM (p : Prop) : p ∨ ¬p. This axiom only slightly affects Lean's type theory. For example, it validates Markov's Principle. The net effect is to make the metatheory classical but the type theory still maintains a "Russian-style" constructivity.

---

Some of my comments in the third paragraph are partly wrong. Leo de Moura said in this Zulip thread that he doesn't consider tactics leaking LEM or AC to be a serious issue. However, he does say that this is only acceptable for Prop so there is a commitment to preserve computabilily. In any case, there is no serious effort from Lean developers to avoid any other axioms such as propositional extensionality and soundness for quotients.

Answer 2

I think given the other two positive answers, I want to temper expectations.

Lean 4 is designed for classical mathematics in mind, and the developers don't have any current plans to support constructive mathematics or compartmentalize axioms (but it does have good support for working with and running computable functions).

After François G. Dorais's very helpful answer, I decided to get some more clarification about Lean 4 from the developers on Zulip. Contrary to the answers given so far, Leonardo de Moura stressed that, due to not being able to work on everything, they have prioritized classical mathematics (even more than Lean 3.4.2). For example the simp tactic uses propext liberally, and the by_cases tactic uses em without checking for decidability first. They have no current plans to compartmentalize axioms.

I encourage anyone who is interested to read Leo's carefully worded statements, but I think it is fair to say that his message is if you really want to do full constructive mathematics, you may have a better user experience with Coq and Agda.

So I think when I said previously that "Lean is classical", I was mostly correct. The rules of Lean are constructive, but most things built on top of that are classical, even outside of mathlib, and classical reasoning is the focus of the Lean developers.

Nonetheless, I think all the answers here (and on Zulip) support that if one isn't interested so much in constructivity as computability, then there is good news: Lean has good support for computable mathematics. As others have stated, Lean keeps track of which functions are computable (even if they use non-constructive proofs inside). While Lean doesn't necessarily let you automatically extract an algorithm from a constructive proof, one can manually pull out that algorithm into a Lean function, prove it is correct (constructively or classically), and run it in Lean.

Answer 3

It's worth noting that there are roughly two different standards of "constructivity" in Lean:

• classical.choice: if #print axioms lists this axiom, then your lemma or definition invokes the axiom of choice (e.g. via LEM) somewhere.
• noncomputable: if classical.choice (or some other axiom) is used to produce data, then this means this data cannot be computably constructed.

Lean will automatically and noisily keep track of the latter for you, if all you care about is that you can computably evaluate your functions and construct your data.

Answering some of your subquestions in the context of the former:

For example, does the user have to constantly worry...

No, see the end of my post. The user can let Lean worry for them.

about LEM being introduced via various forms of automation---like the equation compiler,

I think your only danger here is if classical logic is used to prove termination, but I would guess this never happens

rfl (definitional equality)

No, by definition rfl is just eq.refl, and this does not use classical.choice.

common built-in tactics (simp, rw, etc.)?

Various lemmas in mathlib which use classical.choice are tagged with @[simp]. simp only [safe_lemmas] should be fine, although might still use classical congruence lemmas. rw is safe provided it is used with "safe" lemmas.

Does the user have to avoid many of the definitions in the standard library (since maybe they are not constructive)?

Yes, if we consider Mathlib a standard library, there will be large portions that use classical.choice as an axiom, as little care will have been taken to avoid its use.

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?

This is the important question - you don't need to guess whether a tactic is going to use choice if you can just ask lean to check for you.

Mario Carneiro wrote a small piece of code that provides an @[intuit] attribute that performs the axiom checking automatically, which can be found in this github issue on the mathlib issue tracker.

Answer 4

It is reasonable to ask, "what does constructive mathematics even mean in 2022?"

It certainly owes nothing at all to Brouwer and Heyting's "intuitionism" beyond the rejection of LEM. They firmly rejected the idea that mathematics was symbolic. Modern "constructive mathematics" looks an awful lot like Curry's "formalism". And incidentally, constructive mathematics accepted AC as recently as Bishop.