understanding "Unity and Cohesion" in mathlib

Stream: new members

[Elliot Evans]

I have found this StackExchange thead ("How usable is Lean for constructive mathematics?") via the search functionality of Zulip (searching for "HoTT") which seems to answer my question about the relationship between Lean mathlib and HoTT:

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][3]), 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.

[Elliot Evans]

In this related StackEchange thread ("What are the main differences between Coq and Lean?") Jason Rute gave an answer containing this statement:

[...] There is a strong emphasis on unity and cohesion in this library [Lean Mathlib]. It is constantly refactored to make it work well together. This (according to Lean users) makes it possible to easily combine separate areas of mathematics [...]

I appreciated this statement.

I have a remaining question: Is there documentation or discussion on this "unity and cohesion" or strategy around refactors in the community?

Thank you

[Anne Baanen]

Elliot Evans said:

Hi all, I am new here and I am interested in understanding the broader context that the lean theorem proving community operates within. Does this community use HoTT/Univalent foundations? If not, is there a write-up about the holistic strategy behind ensuring that this library of proofs will be able to scale and grow? Please excuse me if I have asked this in an incorrect or innapropriate manner, I am just trying to jump in :)

Welcome and sorry for the late reply! The most official answer to your question is in the paper on mathlib, especially Section 7 and 8.

[Anne Baanen]

In my opinion, mathlib is good at scaling because refactoring is easy: anything hindering growth is available to be removed, and in general there are little obstacles to refactoring beyond making the technical aspects work and convincing at least one maintainer that it's a good plan. An important aspect is that mathlib basically doesn't care about backwards compatibility.

[Anne Baanen]

Lack of backwards compatibility also means it's the responsibility of any project depending on mathlib to keep up to date. So authors have an incentive to make their project part of mathlib, in order to move the maintenance obligations to the mathlib maintainers. And that means mathlib keeps growing.