Growing Mathlib: maintenance of a large scale mathematical library

DOI10.1007/978-3-032-07021-0_4MaRDI QIDQ6856426zbMATH OpenFDO

Authors Anne Baanen, Matthew Ballard, Johan Commelin, Bryan Gin-Ge Chen, Damiano Testa

Publication date 19 February 2026

Full work available at URL https://doi.org/10.1007/978-3-032-07021-0_4

zbMATH Keywords

formal mathematicslibrary developmentlinting

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Cites work

• A formal proof of the Kepler conjecture
• Abstraction boundaries and spec driven development in pure mathematics
• Automatic test-case reduction in proof assistants: a case study in Coq
• Distributed parallel build for the Isabelle archive of formal proofs
• Experiments with discrimination-tree indexing and path indexing for term retrieval
• Liquid tensor experiment
• Mining the Archive of Formal Proofs
• Teaching mathematics using Lean and controlled natural language
• Term indexing
• The Lean 4 theorem prover and programming language
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Use and abuse of instance parameters in the Lean mathematical library

This page was built for publication: Growing Mathlib: maintenance of a large scale mathematical library

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6856426)