这篇立场论文主张理论级自动形式化，即将完整的理论作为结构化库进行形式化，而不是专注于单个陈述。

作者考察了从孤立定理翻译转向处理整个公理、定义和引理网络的意义。他们探讨了替代观点并确定了该领域中的开放挑战。

为了推进该领域，作者提出了理论级自动形式化的三个有前景的前进方向。