Topic: How old is `mathlib`?
Yury G. Kudryashov (Nov 30 2019 at 00:43):
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
Mario Carneiro (Nov 30 2019 at 02:48):
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 (Nov 30 2019 at 02:50):
The library_dev project is still around at https://github.com/avigad/library_dev
Mario Carneiro (Nov 30 2019 at 02:53):
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 (Nov 30 2019 at 02:59):
This commit by Jeremy looks like the first commit that contains parts that are still in mathlib today
Yury G. Kudryashov (Nov 30 2019 at 03:53):
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 (Nov 30 2019 at 05:05):
One of the reasons it grows so fast is because some people make several PR's per week :wink:
Kevin Buzzard (Nov 30 2019 at 08:53):
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 (Nov 30 2019 at 10:02):
Yury, did you read the mathlib paper? It briefly discusses the history of mathlib and lots of other very interesting things.
Jeremy Avigad (Dec 02 2019 at 01:22):
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.
Last updated: May 16 2021 at 05:21 UTC