Michael Rothgang: Scaling mathlib

Stream: Lean Together 2025

[Matthew Ballard]

A discussion thread for the upcoming talk.

[Michael Rothgang]

Slides: slides.pdf

[Ruben Van de Velde]

Based on available data, scaling mathlib requires beards

[Pietro Monticone]

:video_camera: Video recording: https://youtu.be/cabiomTEWe0

[Michael Rothgang]

For the record: I view the comment above as ironic. (And arguably false, since e.g. Anne or Kim don't wear beards.)

[Michael Rothgang]

Having a beard or being assigned male at birth is not at all correlated to skills for formalisation or working on mathlib tooling. Despite mathlib being a welcoming community, its current diversity numbers are, frankly, pretty terrible (even compared to mathematics in general, whose e.g. gender imbalance/leaky pipeline is also terrible). Changing this is hard, but it's important that we keep working on it.

[Ruben Van de Velde]

Yes, I hope nobody took it seriously - it was based only on the photos in the slides

[Michael Rothgang]

Somebody pointed out that my talk was slightly wrong: Kim Morrison wrote lean4checker (not Mario Carneiro). Sorry for the mix-up. I have corrected the uploaded slides.

[Michael Rothgang]

Furthermore, two tools didn't make it into my talk, but are worth mentioning

• the declarations diff shown in the sticky summary comments is generated by a simple text-based script. That works surprisingly well, but is of course not robust. Alex Best's leaff tool is Lean-aware and a robust version, so using it would be a fantastic improvement.
• Joachim Breitner wrote a tool to check the local confluence of simp lemmas. This is being used on the Lean standard library already (and I'm looking forward to it helping mathlib as well, in the future).

[Michael Rothgang]

Somebody asked: what can you do for mathlib tooling today? Here are some ideas:

• you can implement a new linter, there are lots of ideas just waiting on somebody to implement them
  (three examples: go over the output of the unused variables linter #17715; adapt that to a linter for unused open statements; port some of the missing mathlib3 linters)

• there are many ideas for further queueboard features: I'm happy to mentor/answer questions, and if the existing documentation is not helpful, that can also be changed. See open issues page has some ideas.

• a specific idea: use the queueboard data to create a zulip bot posting about one issue per day which should be triaged.
• what does it take to make leaff usable in mathlib? Can the summary comment use leaff instead?
• in general: keep your eyes open; often an idea just comes along

[Winston Yin (尹維晨)]

Thanks for reviewing the tooling available / under development. As somebody who goes through sporadic waves of mathlib participation, these single-thread new tooling announcements are hard to keep track of. What's a good centralised portal for all these available tools? Can the wiki on the mathlib4 GitHub repo be a good place to host a lot of this information (including a list of tactics)?

[Johan Commelin]

@Michael Rothgang Concerning a zulip bot posting a triage issue: there is of course #triage .
Do you think that bot should learn a few new tricks?

[Bryan Gin-ge Chen]

The script controlling the triage bot is here, though I'm happy to hack on any requests too: (workflow) (python script)