MathCode 终端 AI 把数学证明提速 75 倍:30 秒压到 0.4 秒,数学家从此告别苦役

数学证明一直有两个老大难:Lean 4 编译动辄 30 秒起步,数学家要等;形式化定理难以复用,新证明要从头打地基。

8 月 17 日由 Math-AI 团队开源的 MathCode,把这两个痛点同时砍了一刀:Lean 编译检查从 30 秒压到 0.4 秒,加速 75 倍;每个证明自动命名、存储、成为可导入定理,沉淀成可复用的 Lean 知识库。

它的定位不是「翻译工具」,而是「工程师」:持续读取编译错误、修正思路、重新编译,直到证明通过。这是一条和 AlphaProof、Hunyuan-Prover 完全不同的技术路径——不是训练更大的证明模型,而是把「证明-编译-反馈」的工程流水线压到极限。

怎么把编译从 30 秒压到 0.4 秒

传统 Lean 工作流是「写一段证明 → 退出 → 启动编译器 → 等待 30 秒」。MathCode 的关键工程改动是把 Lean REPL 常驻化:经过一次性预热之后,后续每次编译检查都在同一个 REPL 会话里跑,免去重复启动、重复加载 Mathlib、重复初始化上下文,直接拿到 0.4 秒级响应。

换句话说,这不是模型变聪明了,是工程管道变快了。数学家可以在几分钟内迭代数十次证明策略,而不是在等待中消磨耐心——这跟传统 IDE 的「保存即编译」体验终于对齐了。

知识管理的工程账

MathCode 把证明过程也「产品化」了:

• 自动命名 + 存储:每个证明自动起名、入库,后续可导入复用,而不是证明完就丢;
• 假设固化:对话里的假设被固化成持久化、经过一致性检查的 Lean 声明;
• 自动检索:自动查 leansearch.net 和 Loogle,快速找到已验证的 Mathlib 引理;
• Obsidian 知识图谱:把定理与引理之间的依赖关系可视化为可点击的图谱;
• 子目标并行:支持把复杂定理拆成多个独立子目标,并行证明后再拼接;
• 多规划器:并行运行多个证明规划器,让证明器挑选最优策略。

这意味着数学家从「一次写一段证明」升级为「搭建自己的形式化数学知识库」。这是数学研究范式的隐性革命:几十年来,数学证明的「中间结果」几乎不被复用,每个新证明都从已知定理重新手动链接;MathCode 把这件事自动化了。

它仍然做不了的

需要保持冷静。MathCode 不是「自动证明器」,而是「加速器 + 知识管理工具」。它能做的是:把人类写好的命题自动转 Lean 4 定理、自动编译反馈、自动检索引理、自动沉淀知识图谱。它不能做的是:替你猜下一步该证什么。命题的提出、定理的猜想、证明思路的创造性跳跃,仍然依赖人类数学家。

另外,75 倍加速的前提是「已有 REPL 会话常驻」。冷启动或大型依赖图首次加载时,延迟不会显著低于传统工作流。换句话说,MathCode 的甜点是「中等规模、频繁迭代的证明任务」,不是「一次性大型证明」。

它改变了什么

数学证明的工具栈从「文本编辑器 + LaTeX + 偶尔用用 Lean」正式进入「AI 协作 + 形式化验证 + 知识图谱」的新阶段。这条路径与 OpenAI 8 月初公开的 Astra 系列(用约 2000 美元算力攻克十大数学难题、Lean 4 形式化证明开源)形成呼应——Astra 是「大模型 + 大算力」路径,MathCode 是「工程优化 + 小模型」路径,两条路都在让数学证明变得更可达。

接下来 6 个月,看三个验证点:第一,MathCode 是否能集成进 Lean 官方工具链或 VSCode Lean 插件;第二,Obsidian 知识图谱是否成为数学家发表论文时的标配附件;第三,中文数学社群(尤其是菲尔兹奖新晋得主邓煜、王虹所在的研究领域)会不会把 MathCode 作为日常工具。

数学证明可能永远无法完全自动化,但 MathCode 让它不再像一场漫长的苦役。