# Growing Mathlib: maintenance of a large scale mathematical library

arXiv: https://arxiv.org/abs/2508.21593 · HTML: https://mlsanity.com/paper/2508.21593/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Aug 2025.

## Built on by (most cited first, 5 of 5)

- [DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems](https://mlsanity.com/paper/2510.10815/) (2025)
- [Automatic Textbook Formalization](https://mlsanity.com/paper/2604.03071/) (2026)
- [P3: Joint Program-and-Proof Planning for Verified Code Generation](https://mlsanity.com/paper/2608.09277/) (2026)
- [MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries](https://mlsanity.com/paper/2605.07147/) (2026)
- [Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search](https://mlsanity.com/paper/2605.20244/) (2026)

## Abstract (arXiv)

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.