How old is `mathlib`?

Stream: general

[Yury G. Kudryashov]

Hi, I wonder how old is mathlib (as a project to formalize math in Lean)? I see that the oldest commit is from July 2017 but the second one imports a lot of content from lean/library/data and library_dev.

[Mario Carneiro]

It depends on what you mean. mathlib was originally library_dev, which I think contained some material translated from lean 2. I don't think any lean library projects have truly started from scratch since the beginning

[Mario Carneiro]

The library_dev project is still around at https://github.com/avigad/library_dev

[Mario Carneiro]

Looks like the first few commits on the library_dev repo (Sep 2016) were for super, the sat solver that never made it into mathlib for some reason.

[Mario Carneiro]

This commit by Jeremy looks like the first commit that contains parts that are still in mathlib today

[Yury G. Kudryashov]

Thank you for the explanation. So, the project is very young. That's amazing how fast it came from "simple lemmas about propositional logic" to the current status.

[Johan Commelin]

One of the reasons it grows so fast is because some people make several PR's per week :wink:

[Kevin Buzzard]

One of the reasons that I back the project so publically is that I've seen it grow so quickly. It still amazes me that there are definitions like schemes and manifolds and Noetherian rings, standard BSc and MSc objects, which have appeared in Lean but are in essentially none of the other systems, and when I started just over two years ago it didn't even have complex numbers.

[Patrick Massot]

Yury, did you read the mathlib paper? It briefly discusses the history of mathlib and lots of other very interesting things.

[Jeremy Avigad]

The story is more complicated. Mathlib combined elements of library_dev and Lean's core library. Most of those were in turn ported from Lean 2: https://github.com/leanprover/lean2/tree/master/library, which dates to about 2014. And parts of that library trace all the way back to the original Lean, Lean 0.1. When Mario took over mathlib, he rewrote a lot. But lots of stuff survives from the earlier versions: basic algebraic structures (from semigroups to ordered fields), sets, lists, finsets, nat, int, etc.