Growing Mathlib: maintenance of a large scale mathematical library
Anne Baanen, Matthew Robert Ballard, Johan Commelin, Bryan Gin-ge Chen, Michael Rothgang, Damiano Testa
TL;DR
This paper addresses the challenge of maintaining a rapidly growing large-scale formal library in Lean by outlining an integrated strategy that combines governance, tooling, and engineering practices. It introduces a deprecation system to manage breaking changes, semantic linters to enforce code quality and coherence, and design decisions aimed at speeding up compilation and proof development. The authors also detail mechanisms for tracking and addressing technical debt, porting across major version changes, and scaling code review with automated tooling and triage dashboards. The overall impact is improved upgradeability, reduced maintainer burden, and a set of reusable tools and practices that can transfer to other formal libraries and proof assistants.
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.