# Abstraction boundaries and spec driven development in pure mathematics

arXiv: https://arxiv.org/abs/2309.14870 · HTML: https://mlsanity.com/paper/2309.14870/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Sep 2023.

## Built on by (most cited first, 5 of 5)

- [A Minimal Agent for Automated Theorem Proving](https://mlsanity.com/paper/2602.24273/) (2026)
- [A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Exam](https://mlsanity.com/paper/2504.04945/) (2025)
- [Shaping the Future of Mathematics in the Age of AI](https://mlsanity.com/paper/2603.24914/) (2026)
- [Human agency in initial human-AI proof formalization workflows](https://mlsanity.com/paper/2606.04273/) (2026)
- [Verification abundance, adjudication scarcity: what happens to mathematical knowledge when proof checking becomes free](https://mlsanity.com/paper/2608.28997/) (2026)

## 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.