Growing Mathlib: maintenance of a large scale mathematical library
Programming Languages
2025-10-08 v2 Mathematical Software
History and Overview
Abstract
The Lean mathematical library Mathlib is one of the fastest-growing libraries of formalised mathematics. We describe various strategies to manage this growth, while allowing for change and avoiding maintainer overload. This includes dealing with breaking changes via a deprecation system, using code quality analysis tools (linters) to provide direct user feedback about common pitfalls, speeding up compilation times through conscious library (re-)design, dealing with technical debt as well as writing custom tooling to help with the review and triage of new contributions.
Keywords
Cite
@article{arxiv.2508.21593,
title = {Growing Mathlib: maintenance of a large scale mathematical library},
author = {Anne Baanen and Matthew Robert Ballard and Johan Commelin and Bryan Gin-ge Chen and Michael Rothgang and Damiano Testa},
journal= {arXiv preprint arXiv:2508.21593},
year = {2025}
}
Comments
21 pages, 1 figure. To appear at Conference on Intelligent Computer Mathematics (CICM) 2025 in v2: Minor copy-edits, added one more related reference