3 papers
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.CT2024
Categorical Foundations of Formalized Condensed Mathematics
Dagur Asgeirsson, Riccardo Brasca, Nikolas Kuhn +2
Condensed mathematics, developed by Clausen and Scholze over the last few years, proposes a generalization of topology with better categorical properties. It replaces the concept o…
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…