Scaling mathlib: tooling and automation for an ever-growing mathematics library

Abstract: Maintaining the mathlib library in the presence of continuous growth is a challenge in many aspects. On a technical level, this relies on a fair amount of custom tooling and automation to keep things manageable. I will highlight some recent additions in areas such as deprecations, linting, bots and a new review dashboard. This involves work by many people, including Damiano Testa, Johan Commelin, Mario Carneiro and the author.

This talk is mostly aimed at mathlib contributors (and reviewers), but there will be useful information for mathlib users also.

mathematical softwareMathematics

Audience: researchers in the discipline

( slides | video )

---

Lean Together 2025

Series comments: Most of the talks from the conference are available on YouTube: www.youtube.com/watch?v=ZPPDktjL1Lw&list=PLlF-CfQhukNlzXdQvu1SVt9vcD4--fLlg

---