# Growing Mathlib: maintenance of a large scale mathematical library

## TL;DR

This paper discusses strategies for managing the rapid growth of the Lean Mathlib library, focusing on change management, quality control, and tooling to ensure sustainable development.

## Contribution

It introduces specific methods such as deprecation systems, linters, and custom tooling to handle growth, quality, and technical debt in a large formal mathematics library.

## Key findings

- Effective deprecation reduces breaking changes.
- Code quality tools improve user feedback.
- Design choices speed up compilation.

## 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.