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.

翻译：本文探讨了在交互式定理证明器的辅助下，抽象边界如何帮助驾驭数学研究中的复杂性。尽管文中介绍的许多理念已在数学家群体中隐含应用多年，但我们主张：交互式定理证明器的使用，为这些理念的实现带来了额外的质的提升。