摘要
自动形式化是将非正式自然语言翻译成形式化的、机器可验证的语言。大多数研究集中在单独语句上，而真正的形式化工作本质上是理论层面的：它需要一个完整的公理、定义和引理的网络，才能够陈述目标定理。在这篇立场论文中，我们主张理论层面的自动形式化：将完整的理论形式化，包括它们所有的相互依赖，作为结构化的库。
我们审视这种转变的重要性，讨论替代观点，识别开放挑战，并提出三条有前景的前进路径。我们的自动形式化调查可在 GitHub 查看。
博主点评： 理论层面的自动形式化不仅提高了形式化的效率，还为知识库的构建提供了更加系统的框架。通过整合公理与定义的相互依赖关系，可以显著提升机器理解和推理的能力。未来的研究应关注如何解决现存的挑战，以推动该领域的进一步发展。