Showing 1–5 of 5 results for author: Commelin, J

Growing Mathlib: maintenance of a large scale mathematical library

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

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… ▽ More 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. △ Less

Submitted 29 August, 2025; originally announced August 2025.

Comments: 21 pages, 1 figure. To appear at Conference on Intelligent Computer Mathematics (CICM) 2025

Anatomy of a Formal Proof

Authors: Jeremy Avigad, Johan Commelin, Heather Macbeth, Adam Topaz

Abstract: 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 computer can parse them and check them against the rules of a formal axiomatic foundation. This article describes the experience of working with a proof assistant and considers the impact the technology will have on mathemati… ▽ More 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 computer can parse them and check them against the rules of a formal axiomatic foundation. This article describes the experience of working with a proof assistant and considers the impact the technology will have on mathematics. △ Less

Submitted 4 November, 2024; originally announced November 2024.

Comments: 12 pages

MSC Class: 68V20; 68V15; 03B35

Abstraction boundaries and spec driven development in pure mathematics

Authors: Johan Commelin, Adam Topaz

Abstract: 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 present here have been used implicitly by mathematicians for some time, we argue that the use of an interactive theorem prover introduces additional qualitative benefits in the implementation of these ideas. 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 present here have been used implicitly by mathematicians for some time, we argue that the use of an interactive theorem prover introduces additional qualitative benefits in the implementation of these ideas. △ Less

Submitted 26 September, 2023; originally announced September 2023.

Comments: To appear in a special volume of the Bull. Amer. Math. Soc.; 14 pg.; feedback welcome!

Formalizing the Ring of Witt Vectors

Authors: Johan Commelin, Robert Y. Lewis

Abstract: The ring of Witt vectors $\mathbb{W} R$ over a base ring $R$ is an important tool in algebraic number theory and lies at the foundations of modern $p$-adic Hodge theory. $\mathbb{W} R$ has the interesting property that it constructs a ring of characteristic $0$ out of a ring of characteristic $p > 1$, and it can be used more specifically to construct from a finite field containing… ▽ More The ring of Witt vectors $\mathbb{W} R$ over a base ring $R$ is an important tool in algebraic number theory and lies at the foundations of modern $p$-adic Hodge theory. $\mathbb{W} R$ has the interesting property that it constructs a ring of characteristic $0$ out of a ring of characteristic $p > 1$, and it can be used more specifically to construct from a finite field containing $\mathbb{Z}/p\mathbb{Z}$ the corresponding unramified field extension of the $p$-adic numbers $\mathbb{Q}_p$ (which is unique up to isomorphism). We formalize the notion of a Witt vector in the Lean proof assistant, along with the corresponding ring operations and other algebraic structure. We prove in Lean that, for prime $p$, the ring of Witt vectors over $\mathbb{Z}/p\mathbb{Z}$ is isomorphic to the ring of $p$-adic integers $\mathbb{Z}_p$. In the process we develop idioms to cleanly handle calculations of identities between operations on the ring of Witt vectors. These calculations are intractable with a naive approach, and require a proof technique that is usually skimmed over in the informal literature. Our proofs resemble the informal arguments while being fully rigorous. △ Less

Submitted 23 December, 2020; v1 submitted 6 October, 2020; originally announced October 2020.

Journal ref: Proceedings of Certified Programs and Proofs (CPP 2021)

Formalising perfectoid spaces

Authors: Kevin Buzzard, Johan Commelin, Patrick Massot

Abstract: Perfectoid spaces are sophisticated objects in arithmetic geometry introduced by Peter Scholze in 2012. We formalised enough definitions and theorems in topology, algebra and geometry to define perfectoid spaces in the Lean theorem prover. This experiment confirms that a proof assistant can handle complexity in that direction, which is rather different from formalising a long proof about simple ob… ▽ More Perfectoid spaces are sophisticated objects in arithmetic geometry introduced by Peter Scholze in 2012. We formalised enough definitions and theorems in topology, algebra and geometry to define perfectoid spaces in the Lean theorem prover. This experiment confirms that a proof assistant can handle complexity in that direction, which is rather different from formalising a long proof about simple objects. It also confirms that mathematicians with no computer science training can become proficient users of a proof assistant in a relatively short period of time. Finally, we observe that formalising a piece of mathematics that is a trending topic boosts the visibility of proof assistants amongst pure mathematicians. △ Less

Submitted 28 May, 2020; v1 submitted 27 October, 2019; originally announced October 2019.

Comments: Final version, with small additions requested by referees. 22 pages. See also https://leanprover-community.github.io/lean-perfectoid-spaces/

Journal ref: CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, Pages 299-312