Evolving of Mathlib

Stream: mathlib4

[Beryl Zhang]

Hi all, thanks for your contributions to the community.

I was using Mathlib 4.18.0 before, and I realized that over the last 6 months, it has evolved to Mathlib 4.25.0-rc2. I'm wondering about the changes. I was told that there are more than 200k theorems in the library now, but when I was testing previously, the statistics showed around 130k.

I want to know where I can find these numbers and new statistics for the newer version of Mathlib. Thanks for your help!

[Rémy Degenne]

There is a stats page here: https://leanprover-community.github.io/mathlib_stats.html

[Beryl Zhang]

Thanks! That's very helpful!

[Martin Dvořák]

Mathlib 4.18.0 is my most favorite version!

[Weiyi Wang]

What's special about 4.18.0?

[Beryl Zhang]

I use it mainly for my research, because the dataset I'm using is built based on Lean 4 and Mathlib 4.18.0. I think that when the Mathlib updated, potentially these dataset/benchmarks need to be updated as well, is it? Also, I have to say, something building the environment is painful!

[Kevin Buzzard]

If you mean "building mathlib is painful" then do you know about lake exe cache get

[Beryl Zhang]

not only mathlib, I mean the whole Lean environment, and other library dependencies. But probably that's just our machine/server is not good :joy:

[Martin Dvořák]

Weiyi Wang said:

What's special about 4.18.0?

It was the last stable version that contained LinearOrderedField and similar classes.