Abstraction boundaries and spec driven development in pure mathematics
Not on the map. Why?
Abstract (arXiv)
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.
Key facts. Cited by 5 papers in the map (data through 14 Oct 2026). First posted on arXiv 26 Sep 2023.
Builds on
No reference list yet.
Built on by
Citing papers per year: 2025: 1; 2026: 4.
5 papers.
- 2026A Minimal Agent for Automated Theorem Provingcited by 18
- 2025A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Examcited by 3
- 2026Shaping the Future of Mathematics in the Age of AIcited by 2
- 2026Human agency in initial human-AI proof formalization workflowscited by 0
- 2026Verification abundance, adjudication scarcity: what happens to mathematical knowledge when proof checking becomes freecited by 0
- 2026Verification abundance, adjudication scarcity: what happens to mathematical knowledge when proof checking becomes free29 Aug 2026
- 2026Human agency in initial human-AI proof formalization workflows2 Jun 2026
- 2026Shaping the Future of Mathematics in the Age of AI26 Mar 2026
- 2026A Minimal Agent for Automated Theorem Proving27 Feb 2026
- 2025A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Exam7 Apr 2025