17
$\begingroup$

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.

$\endgroup$

4 Answers 4

8
$\begingroup$

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.

$\endgroup$
4
  • 1
    $\begingroup$ "No parts of the standard Lean 2/3/4 library will surreptitiously introduce LEM or AC [...] they aren't used outside the Classical namespace." I think lt_or_eq_of_le in both Lean 3.4.2 and Lean 3.42.0c (community edition) is a counterexample: #print axioms lt_or_eq_of_le gives classical.choice among the others axioms. (This theorem isn't currently in Lean 4). Maybe this is a bug or oversight in Lean 3. $\endgroup$
    – Jason Rute
    Mar 20 at 21:08
  • $\begingroup$ Also, I'm not clear if you are talking about tactics as well, but in Lean 3.42.0c I've also noticed some tactics like by_cases do not fall under the classical namespace, but still allow you to prove LEM. However, this doesn't seem to be true for Lean 3.4.2 or Lean 4, so maybe a lot of my confusion is based around the community edition of Lean 3, which is the currently most used Lean version but will be replaced with Lean 4. I guess this is a question for the Lean 4 developers if they intend to keep a clear separation of classical reasoning in base Lean 4. $\endgroup$
    – Jason Rute
    Mar 20 at 21:09
  • $\begingroup$ Lean 3 had a couple of issues; I only use Lean 4 now and Lean 3's issues are fading from my memory. This is a bug: the ordering library in Lean 3 only made sense for decidable orderings but decidability was not part of the definition. See here, section 4, for a brief discussion of constructive aspects of order theory. That was annoying and I couldn't use any of the ordering classes, even for decidable orderings. Fortunately, if you don't use these classes then lt_or_eq_of_le can't trigger. $\endgroup$ Mar 20 at 22:48
  • $\begingroup$ I really can't speak about the community edition of Lean 3. I used some of the first few editions but quickly moved to Lean 4. $\endgroup$ Mar 20 at 22:49
7
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ I'm beginning to see that there is a hierarchy. If one just wants computable functions, that is easy to do in Lean since, as you said, Lean keeps track of this for you. (It also doesn't hurt that Lean 4 is a programming language.) That would likely satisfy some folks whose only need of constructive mathematics is to keep track of computational information in proofs. But I don't think it is fair to call it constructive mathematics. $\endgroup$
    – Jason Rute
    Mar 21 at 23:13
  • 1
    $\begingroup$ Avoiding classical.choice seems harder, but I think you and François have convinced me it isn't Earth-shattering hard, if you avoid mathlib, by_cases, by_contradiction, and use @[intuit] to keep your proofs honest. Avoiding the other axioms, especially propext seems much more challenging. For example Leo just said on Zulip that much of Lean 4's automation, such as simp, depends on propext. $\endgroup$
    – Jason Rute
    Mar 21 at 23:13
  • $\begingroup$ In Lean 3, by_cases and by_contradiction are often choice-free, they just fallback on choice if they need it. With @[intuit] there is no need to avoid them. $\endgroup$
    – Eric
    Mar 22 at 0:16
  • $\begingroup$ Regarding whether noncomputable counts as constructive mathematics; I've seen a number of new users who are surprised that can't extract the witness from their "constructive" proof of an existential. If they want this version of constructivity, then they may end up avoiding Prop (in this case, with sigma instead of Exists); which makes noncomputable relevant. $\endgroup$
    – Eric
    Mar 22 at 0:32
  • 2
    $\begingroup$ I just want to point out that noncomputable is only checked by the frontend, not the kernel, in case this matters to anyone. Probably more relevant to constructive mathematics would be whether a definition is able to reduce without getting stuck, but Lean doesn't have any mechanism to keep track of this property. $\endgroup$ Mar 22 at 20:53
5
$\begingroup$

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.

$\endgroup$
3
$\begingroup$

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.

$\endgroup$
3
  • 1
    $\begingroup$ Care if I edit this and add links from Stanford Encyclopedia of Philosophy? Formalism Intuitionistic Logic Constructive Mathematics since many will not read this comment. $\endgroup$
    – Guy Coder
    Mar 27 at 11:45
  • 2
    $\begingroup$ There seems from my point of view to be a trend moving toward thinking of constructivism via type theoretic formal foundations (eg IHOL, MLTT, HoTT, etc) and via categorical semantics (topos and there higher category versions). I like this since it seems more mathematical to me (we have an interesting and mathematically useful syntax and semantics) as opposed to the vague philosophical positions of the past, but that might be just my point of view. $\endgroup$
    – Jason Rute
    Mar 27 at 12:27
  • 1
    $\begingroup$ I feel whatever Bishop meant by AC (and Andre’s answer in that link is enlightening) is not what Lean means since Lean has Prop. (And it also probably isn’t the version of AC in HoTT either.) $\endgroup$
    – Jason Rute
    Mar 27 at 12:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.