Showing math.HOShow all
2 papers · 1 filter
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…