{"ID":2876753,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2508.21593","arxiv_id":"2508.21593","title":"Growing Mathlib: maintenance of a large scale mathematical 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.","short_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 too...","url_abs":"https://arxiv.org/abs/2508.21593","url_pdf":"https://arxiv.org/pdf/2508.21593v2","authors":"[\"Anne Baanen\",\"Matthew Robert Ballard\",\"Johan Commelin\",\"Bryan Gin-ge Chen\",\"Michael Rothgang\",\"Damiano Testa\"]","published":"2025-08-29T12:49:58Z","proceeding":"cs.PL","tasks":"[\"cs.PL\",\"cs.MS\",\"math.HO\"]","methods":"[]","has_code":false}