Papers With

← All papers
First page of Growing Mathlib: maintenance of a large scale mathematical library

Growing Mathlib: maintenance of a large scale mathematical library

Anne Baanen, Matthew Robert Ballard, Johan Commelin, Bryan Gin-ge Chen, Michael Rothgang, Damiano Testa

cs.PL Aug 29, 2025 · v1
mathlib tooling meta-study formalization
Read PDF arXiv abstract Code
TL;DR
Describes strategies, linters, deprecation systems, and custom tooling for maintaining the Lean Mathlib library.
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.
Problem

Mathlib, one of the fastest-growing libraries of formalized mathematics in Lean, faces challenges in managing growth while allowing change and avoiding maintainer overload.

Approach

The paper describes strategies for managing Mathlib's growth: a deprecation system for handling breaking changes, semantic linters for user feedback on common pitfalls, compilation speed optimizations through conscious library design, technical debt tracking, and custom tooling for review and triage of contributions.

Results

Mathlib now contains 1.9 million lines of code across a broad range of mathematical subjects. The paper documents concrete practices including the VelCom-based Speedcenter for benchmarking, the Queueboard for PR triage, and the deprecation system that enables downstream projects to keep up with API changes.