Zulip Chat Archive
Stream: Lean Together 2024
Topic: Patrick's talk
Kevin Buzzard (Jan 09 2024 at 14:08):
What are the units on the y axis?
Screenshot-from-2024-01-09-14-07-30.png
Alex J. Best (Jan 09 2024 at 14:08):
number of files?
Kevin Buzzard (Jan 09 2024 at 14:08):
Yes it must be -- thanks (we hit 4000 files recently)
Kim Morrison (Jan 09 2024 at 14:14):
Conveniently it means the mathlib3 / mathlib4 crossover is actually a crossover!
Last updated: May 02 2025 at 03:31 UTC