3 papers
cs.PL2025
Growing Mathlib: maintenance of a large scale mathematical library
Anne Baanen, Matthew Robert Ballard, Johan Commelin +3
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 ch…
math.HO2024
Anatomy of a Formal Proof
Jeremy Avigad, Johan Commelin, Heather Macbeth +1
Interactive proof assistants make it possible for ordinary mathematicians to write definitions and theorems in a formal proof language, like a programming language, so that a compu…
math.HO2023
Abstraction boundaries and spec driven development in pure mathematics
Johan Commelin, Adam Topaz
In this article we discuss how abstraction boundaries can help tame complexity in mathematical research, with the help of an interactive theorem prover. While many of the ideas we…