Zulip Chat Archive

Stream: general

Topic: three years

Rob Lewis (Jul 21 2020 at 08:35):

Oliver Nash (Jul 21 2020 at 08:56):

Patiently have you been waiting to post this :wink:

Gabriel Ebner (Jul 21 2020 at 08:59):

Happy birthday, stdlib? As far as I remember, mathlib was born a month later: https://github.com/leanprover-community/mathlib/commit/4320c41797cdc539656d17c3875cb15f476e7326

Rob Lewis (Jul 21 2020 at 09:00):

This is a deep question. Is a project's identity tracked by its name or its git history?

Marc Huisinga (Jul 21 2020 at 09:22):

changing your name should not reset your birthday

Kevin Buzzard (Jul 21 2020 at 10:36):

This surprises me a bit, because my 3rd birthday for beginning to use Lean was, I thought, the day Tom Hales said in Cambridge "my proposal is Lean", on 10th July 2017. What did Lean look like on that date?

Kevin Buzzard (Jul 21 2020 at 10:36):

Maybe I only came to the chat a few days later.

Kevin Buzzard (Jul 21 2020 at 10:37):

https://www.newton.ac.uk/seminar/20170710100011001

Rob Lewis (Jul 21 2020 at 10:40):

Most of the library was in core. There was another repo library_dev that was like a proto-mathlib.

Last updated: Dec 20 2023 at 11:08 UTC