Abstraction boundaries and spec driven development in pure mathematics
Johan Commelin, Adam Topaz
TL;DR
This paper explores how abstraction boundaries, supported by interactive theorem provers, can reduce complexity in pure mathematics research, offering both implicit and explicit benefits.
Contribution
It introduces the use of interactive theorem provers to explicitly implement and enhance abstraction boundaries in mathematical research.
Findings
Abstraction boundaries help manage complexity in mathematics.
Interactive theorem provers provide qualitative benefits.
Explicit use of theorem provers improves mathematical practice.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Artificial Intelligence in Games · History and Theory of Mathematics