Growing Mathlib: maintenance of a large scale mathematical library
Not on the map. Why?
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.
Key facts. Cited by 5 papers in the map (data through 14 Oct 2026). First posted on arXiv 29 Aug 2025.
Builds on
No reference list yet.
Built on by
Citing papers per year: 2025: 1; 2026: 4.
5 papers.
- 2025DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theoremscited by 8
- 2026Automatic Textbook Formalizationcited by 8
- 2026P3: Joint Program-and-Proof Planning for Verified Code Generationcited by 2
- 2026MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Librariescited by 1
- 2026Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Searchcited by 1
- 2026P3: Joint Program-and-Proof Planning for Verified Code Generation10 Aug 2026
- 2026Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search18 May 2026
- 2026MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries8 May 2026
- 2026Automatic Textbook Formalization3 Apr 2026
- 2025DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems12 Oct 2025