当AI开始涉足数学证明，我们如何确定它不是在“一本正经地胡说八道”？ProofForge给出了一个硬核答案：AI生成的证明必须在Lean 4中通过编译，否则就不算数。这个项目通过多智能体流水线，将复杂问题分解、证明、形式化，最终交给Lean内核做终极裁判。
ProofForge究竟是什么？
ProofForge是一个专注于机器验证的AI智能体流水线，目标是产出能够在Lean 4和Mathlib环境中编译通过的数学证明。与传统AI直接输出自然语言证明不同，ProofForge的产出物是形式化代码，必须经过Lean内核的严格检查。简单来说，它不是一个“证明生成器”，而是一个“证明编译器”——AI负责拆解和书写，Lean负责裁决对错。
AI智能体如何分工协作完成证明？
ProofForge的核心是一套多智能体协作流程。整个流水线分为三个关键步骤：
首先，智能体会对问题进行分解（decompose a problem），将一个复杂的数学命题拆解成若干个可管理的小块；接着，各个智能体分别证明这些片段（prove the pieces），形成初步的证明思路；最后，系统将这些片段在Lean中形式化（formalize them in Lean），转换成严格的类型论代码。这个过程不是一步到位的，而是通过分工降低单一AI出错的概率。
为什么说“AI证明了它”不能只靠信任？
在ProofForge的框架下，“AI证明了它”不是一个信任问题，而是一个编译问题。Lean内核会重新检查证明中的每一步（rechecks every step），任何逻辑漏洞或类型错误都会导致编译失败。项目通过 axioms命令确保证明只依赖标准公理，并且从不使用native_decide这种可能引入黑箱计算的策略。这意味着：一个错误的证明根本无法编译通过，检查器要么接受，要么拒绝，没有中间地带。
ProofForge已经取得了哪些实际成果？
ProofForge已经向Google DeepMind的formal-conjectures项目贡献了多个证明。截至文章撰写时，大部分贡献已经合并，且所有合并的证明都经过了内核验证（kernel-verified）。目前仍有一个开放中的贡献：编号为#4360的提案，目标是给出isUnitaryPerfect_87360的一个更快证明。这些成果证明了该流水线不仅在理论上可行，而且在真实的形式化数学社区中产生了实际价值。
Lean源码和仓库结构是怎样的？
对于希望查看或验证代码的开发者，ProofForge的仓库结构相对清晰。前两个证明的Lean源码直接存放在本仓库的proofs/目录下，方便快速查阅和测试；而后续的贡献则合并到上游仓库（upstream in the repository they were contributed to），与原项目的代码库保持同步。这种设计既保留了本地示例的完整性，又确保了对上游项目的无缝贡献。
这个仓库与Erdős相关项目有什么关系？
ProofForge的覆盖范围与Erdős问题形式化密切相关。该仓库专注于Lean 4形式化工作，意味着它处理的很多数学命题可能涉及组合数学、数论等Erdős曾经深入研究过的领域。通过将AI证明能力与Lean的形式化严格性结合，ProofForge为大规模数学猜想的形式化验证提供了一条可复用的技术路径。
说到底，ProofForge最吸引人的地方，是它把AI从“概率性的文本生成器”拉回到了“可验证的工程实践”中。当整个行业都在追逐更大参数、更长上下文时，它却固执地在门口加了一道Lean编译器——进不来，就证明你说错了。这种“不近人情”的严谨，或许正是当前AI+数学最缺的一味药。
我认为：AI的聪明终究是借来的，唯有内核的编译指令才是自己的。倘若每一步证明都要靠人情与信任来担保，那数学的殿堂便与赌场无异；ProofForge好歹在赌场门口设了验钞机，虽然叮当作响，却也让人安心了几分。
#定理证明
© 版权声明
文章版权归作者所有，未经允许请勿转载。
