Zulip Chat Archive

Stream: mathlib4

Topic: 7000 files

Kenny Lau (Jul 28 2025 at 14:13):

image.png

Kenny Lau (Jul 28 2025 at 14:13):

what is the 7000th file?

Kenny Lau (Jul 28 2025 at 14:15):

From a simple browsing of commits, it seems like Mathlib/Analysis/SpecialFunctions/Integrals/PosLogEqCircleAverage.lean was the 7000th file

Kenny Lau (Jul 28 2025 at 14:15):

added by @Stefan Kebekus :tada:

Kenny Lau (Jul 28 2025 at 14:17):

image.png

It looks like the CI counts things differently though?

Stefan Kebekus (Jul 28 2025 at 14:17):

Thanks for the :tada:

But is the number of files a reason to celebrate … or a reason for concern?

Michael Rothgang (Jul 28 2025 at 14:18):

To me, mathlib growing is a reason to celebrate. (Mathlib needing many lines is a sign we need better automation, but that's a continuous process.)

Stefan Kebekus (Jul 28 2025 at 14:18):

Ok, let's celebrate then. I am all for it.

Kenny Lau (Jul 28 2025 at 14:19):

I think I have a better algorithm

Kenny Lau (Jul 28 2025 at 14:20):

ah, by the algorithm of just looking at the line count of Mathlib.lean, we're at 6665 files instead.

Aaron Liu (Jul 28 2025 at 14:20):

Are we counting Std and Batteries as files?

Kenny Lau (Jul 28 2025 at 14:23):

who knows

Eric Wieser (Jul 28 2025 at 14:31):

Batteries + Aesop + ... yes, Std no

Last updated: Dec 20 2025 at 21:32 UTC