理论级自动形式化：从孤立命题到统一的形式知识库

自动形式化旨在将非正式的自然语言转化为机器可验证的形式语言。当前研究多聚焦于单个语句的翻译，但实际的形式化工作本质上是理论级的：在陈述目标定理之前，需要构建完整的公理、定义和引理网络。这篇立场论文主张推进理论级自动形式化，即将完整理论及其所有相互依赖关系形式化为结构化知识库。

作者分析了这一转向的重要意义，探讨了不同观点，指出了当前面临的开放挑战，并提出了三条可行的发展路径。研究强调，构建统一的形式知识库将极大提升数学和计算机科学领域的自动化验证效率。相关综述资料已开源发布，为后续研究提供参考。