Theorem（定理）指在公理体系中经严格推导证明为真的数学命题，是数学与形式化方法的核心对象。近两年，随着大语言模型介入自动定理证明与形式化验证，定理的证明、检验与检索方式正被显著改写，成为 AI 与数学交叉领域最活跃的方向之一。
Theorem 证明的近期进展
当前焦点与观察点
当前讨论集中在三个层面。其一是可信性：Claude 完成的费马大定理形式化证明之所以受关注，正是因为其正确性由 Lean 编译器独立检验，而非依赖模型自述，这为「AI 证明需机器可验证」树立了范式。其二是效率：SCOPE、NanoProof 等工作试图把自动定理证明从大算力专属推向更开放的生态。其三是外延扩展：Hempel 统计模糊性等科学哲学问题与 Causal AI 的结合（相关论文），以及博弈论 Minimax Theorem 在策略推理中的应用（相关讨论），显示定理思维正渗透到因果推断与决策理论等相邻领域。值得观察的是，AI 生成的形式化证明能否覆盖更广泛的数学分支，以及开源工具链能否跟上头部实验室的节奏。