MathCode 把数学证明变成编程任务

Math-AI 团队开源的 MathCode，正在把 Coding Agent 从“替开发者写代码”推进到“替数学研究者写证明”。截至 2026 年 8 月 16 日，项目公开版本已加入 Tree of Subgoals、TheoremLib、AxiomLib、Guide of Plans、Blueprint，以及可自定义的 Tools 和 Skills，形成了一套围绕 Lean 4 的数学形式化工作流。

MathCode 是一个内置数学形式化引擎的终端 Coding Agent：用户输入自然语言数学问题后，它会尝试将问题转换成 Lean 4 定理，再调用模型、证明工具和知识库搜索可被 Lean 内核检查的证明。项目采用开源方式发布，数学形式化与证明管线建立在 AUTOLEAN 项目之上。

这不是又一个“数学聊天机器人”。MathCode 真正值得关注的地方，是它没有把语言模型生成的一段推导当成最终答案，而是要求最终结果进入形式化证明系统接受检查——模型可以猜、可以试，也可以反复修改，但不能靠语言流畅度蒙混过关。

MathCode做的不是解题，而是建立可验证证明

形式化证明是把数学命题与推导过程写成机器可检查表达式的方法。传统数学答案主要由人类阅读并判断逻辑是否成立，而 Lean 4 会把定义、类型、前提和每一步推导交给一个相对精简的内核验证，证明脚本只要存在类型不匹配、遗漏条件或非法推导，就无法正常通过检查。

MathCode 的基本工作流可以概括为五步：

1. 接收自然语言描述的数学问题；
2. 将题目翻译为 Lean 4 中的定义、变量、假设和待证定理；
3. 把总目标拆成多个可以逐步处理的子目标；
4. 调用模型、定理库、策略和外部工具尝试构造证明；
5. 将候选证明交给 Lean 4 检查，并根据错误信息继续修正。

这个流程与普通 Coding Agent 修复编译错误很相似。普通 Agent 会读代码、运行编译器、观察报错，再修改代码；MathCode 则会生成 Lean 证明、读取类型检查与目标状态，再调整定理表达或证明策略。Lean 在这里既是编程语言，也是不会因为回答“看起来合理”就放行的裁判。

MathCode 默认后端依赖 Codex CLI，但它本身并不是一个新的基础模型。更准确地说，MathCode 是一个面向数学任务设计的 Agent 系统，核心竞争力来自形式化管线、状态管理、知识复用和工具编排，而不是一组独立训练并公开权重的模型参数。

这一点也决定了它的实际表现会受后端模型影响。更强的代码与推理模型通常更擅长理解 Lean 报错、选择引理和调整证明，但即使底层模型相同，是否拥有持久化环境、结构化子目标以及可检索的定理库，也会显著影响复杂任务能否持续推进。

0.1.0的重点，是让Agent学会管理证明过程

Tree of Subgoals 是把证明目标组织成树状结构的机制。复杂定理通常无法通过一次生成完成，Agent 需要把主命题拆成若干引理，再将每个引理继续分解；如果只保存一段线性对话，模型很容易忘记哪些分支已经解决、哪些假设仍未使用。

子目标树解决的是数学 Agent 的项目管理问题。它让系统可以追踪每个分支的状态，失败时只回退局部步骤，而不是推翻整段证明重新生成；对于包含分类讨论、归纳证明或多层辅助引理的任务，这比单轮提示词更接近人类使用证明助手时的真实工作方式。

Persistent Lean REPL 是一个持续保留 Lean 会话状态的交互环境。普通的一次性执行每次都要重新加载上下文，而持久化 REPL 可以保留已经导入的模块、声明的变量、构造的定义和当前证明状态，减少重复初始化，也方便 Agent 根据上一轮错误继续工作。

TheoremLib 是用于积累和复用定理的知识库。数学证明高度依赖已有结论，同一个关于整除、奇偶性、序关系或代数结构的引理，不应在每道题里重新证明；可复用定理库让 Agent 更像在一个持续成长的代码仓库里工作，而不是每次打开一张空白草稿纸。

AxiomLib 是用于管理公理或外部假设的组件。它提高了处理不同数学体系和未完整形式化背景知识的灵活性，但也带来一个必须强调的边界：Lean 能验证的是“结论能否从当前公理和假设推出”，并不自动保证用户加入的公理真实、相容或足够保守。

因此，AxiomLib 既是能力，也是风险入口。如果 Agent 为了让证明通过而引入过强假设，甚至直接加入与目标等价的公理，形式上依然可能得到可检查结果，但数学价值已经被掏空；严肃使用时必须审计新增公理、未证明声明以及任何可能绕过证明义务的机制。

Guide of Plans 和 Blueprint 负责把证明意图显式化。大模型直接面对一个复杂 Lean 目标时，容易陷入局部语法修补，而计划与蓝图可以先规定整体路线，例如先建立边界条件、再证明单调性、最后组合已有引理，从而把“下一行写什么”提升为“整条证明为什么这样走”。

Tools 和 Skills 则把 MathCode 从固定流程扩展为可组合系统。Tools 更接近可调用的外部能力，Skills 更接近可复用的任务方法或领域经验；开发者可以针对代数、数论、几何或特定代码库补充工具与技能，而不必修改整个 Agent 主循环。

它与通用Coding Agent有什么不同

MathCode 与通用 Coding Agent 的最大区别，是最终验收标准从“程序是否运行”变成“证明是否被形式化内核接受”。两者都使用模型规划、工具调用和错误反馈，但数学形式化对定义精度、隐含前提和逻辑闭合的要求更高。

| 对比维度 | MathCode | 通用 Coding Agent | 普通数学聊天模型 | |---|---|---|---| | 核心任务 | 数学形式化与 Lean 4 证明 | 编写、修改和调试软件 | 生成自然语言解答 | | 最终验证 | Lean 内核检查 | 编译器、测试与运行结果 | 通常依靠人工阅读或答案匹配 | | 状态载体 | 证明目标、上下文、子目标树 | 文件、终端、版本差异 | 对话上下文 | | 知识复用 | TheoremLib、AxiomLib、Skills | 代码库、依赖、文档 | 模型参数与检索内容 | | 失败反馈 | 类型错误、未完成目标、策略失败 | 编译错误、测试失败、运行异常 | 缺少稳定的机器反馈 | | 主要风险 | 形式化错误、错误公理、规格偏差 | 引入缺陷、破坏接口、执行风险 | 幻觉与推理跳步 | | 输出可信度 | 证明通过不等于题目形式化正确 | 测试通过不等于软件完全正确 | 表述合理不等于结论正确 |

MathCode 相比普通数学模型更可靠，但并没有消灭幻觉。它只是把幻觉更早地暴露为类型错误、未知定理、未完成目标或证明失败，让错误不容易伪装成一篇读起来顺畅的答案。

MathCode 相比通用 Coding Agent 更垂直，也更依赖领域基础设施。一个成熟的软件 Agent 可以依靠测试套件判断改动是否正确，而数学问题往往先要完成自然语言到形式化规格的转换；如果命题在第一步就被翻译错了，后续证明再严谨，也只是在证明另一个命题。

最难的部分，其实发生在Lean开始验证之前

自然语言形式化是 MathCode 整条链路中最容易被低估的环节。题目里的“任意”“存在”“唯一”“连续”“有限”或“通常情况下”都可能对应不同的量词、类型和前提，漏掉一个定义域限制，就会让原命题变成假命题或无意义命题。

例如，“偶数的平方仍是偶数”在人类看来没有歧义，但系统需要明确变量属于自然数还是整数、偶数如何定义、平方使用什么运算，以及结论要输出存在性证明还是调用既有引理。对于竞赛题和研究命题，形式化成本会高得多，因为图形关系、默认背景和省略条件往往散落在上下文里。

规格正确性因此比证明通过更重要。Lean 可以保证某段证明符合已经写下的形式化命题，却不能自动确认这段形式化命题忠实表达了用户最初的问题；这与软件工程中的“程序符合规格，但规格本身写错”是同一种风险。

MathCode 的理想使用方式不是完全无人监督，而是让人类检查命题、关键定义和新增公理，让 Agent 承担重复搜索、语法修补和子目标推进。对于研究数学家、形式化工程师和 Lean 学习者，这种人机分工比追求一次输入、自动吐出完整证明更现实。

目前还不能用跑分证明它是“前沿”

MathCode 官方项目目前强调的是系统能力与工作流，而不是一套足以横向比较的标准化评测结果。现有公开材料没有给出可用于验证“前沿”定位的完整基准表，包括任务集、后端模型、推理预算、成功率、平均耗时以及是否允许人工干预等关键数据。

缺少统一跑分意味着用户不应把“Frontier Mathematical Coding Agent”直接理解为已经超过所有数学模型或证明 Agent。一个数学 Agent 的成功率可以通过增加采样次数、扩大上下文、调用更强后端或提供更多人工提示得到明显改变，如果不公开推理预算，单独报告通过率几乎没有比较意义。

真正有价值的后续数据至少应包含以下几类：

• 自然语言命题被正确形式化的比例；
• Lean 证明一次通过率与多轮修复后的通过率；
• 每道题平均模型调用次数、总耗时和计算成本；
• 引入新公理或未证明占位符的比例；
• 在 MiniF2F、ProofNet 等形式化任务集上的可复现实验；
• 更换不同后端模型后的性能变化；
• 人工审核前后，形式化规格错误率的差异。

在这些数据补齐之前，MathCode 最可信的卖点不是“数学能力已经达到某个排名”，而是它把 Agent 工程中的状态、计划、工具和知识库带进了 Lean 证明流程。对于开发者而言，这种架构价值已经足够明确，但它与基准领先仍是两回事。

安装门槛不高，使用门槛仍然很高

MathCode 当前面向 macOS arm64 和 Linux x86_64 环境，默认后端需要 Codex CLI。项目提供安装脚本与打包运行环境，初始化后会安装用户级命令；证明输出默认写入 LeanFormalizations/，同时提供浏览器界面入口。

操作系统和运行时只是表面门槛，真正的使用门槛来自 Lean 与数学形式化本身。用户如果不理解目标状态、类型、定理声明和公理边界，就很难判断 Agent 是在解决原问题、修改问题，还是用不恰当假设绕过问题。

Obsidian 知识图谱体现了项目对长期知识积累的重视。证明、定理、计划和概念关系如果只存在于终端日志中，很难被后续任务复用；图谱化管理可以帮助用户查看某个结论依赖哪些定义与引理，也方便把一次证明转化为未来可检索的资产。

这种设计让 MathCode 更像“数学研究工作台”，而不是单次答题工具。它最适合的场景包括 Lean 项目原型、课程证明练习、已有论文结论的形式化尝试，以及为特定数学领域建设可持续扩展的定理库。

开源的意义，在于证明过程可以被审计

MathCode 选择开源，比单纯提供一个在线答题界面更符合形式化数学的需求。开发者可以检查提示流程、工具权限、定理来源、运行环境和证明产物，也可以定位系统究竟在哪一步误解了命题，而不是只看到一个成功或失败的最终状态。

开源还允许社区围绕不同数学领域构建专用 Skills。数论证明与实分析证明使用的库、策略和常见模式差异很大，一个统一提示词很难覆盖所有场景；让领域用户贡献计划模板、检索工具和定理集合，比只依赖下一代更大的模型更有持续价值。

MathCode 现阶段最大的优势是方向正确，而不是产品已经成熟。它抓住了数学 Agent 的核心矛盾：模型擅长提出候选步骤，却不擅长独立保证正确性；Lean 擅长验证正确性，却不擅长从自然语言中主动寻找证明，两者组合后才能形成“生成—检查—修正”的闭环。

MathCode 现阶段最大的短板则是评测和规格审计仍不充分。一个证明通过 Lean 检查，只能说明它在给定定义和假设下成立；要成为真正可靠的数学助手，系统还必须证明自己没有误读题目、滥用公理、错误引用定理或用不可接受的占位机制完成任务。

我们的判断：它更像数学版IDE Agent，而不是数学版ChatGPT

MathCode 最值得开发者关注的定位，是“围绕 Lean 4 构建的数学版 IDE Agent”。它把命题形式化、证明计划、子目标管理、库检索、工具调用和内核验证放进同一条工作流，这比单纯让大模型输出 Lean 代码更接近可持续使用的产品。

MathCode 短期内不会替代数学家，也不会让没有 Lean 基础的用户稳定解决研究级问题。自然语言规格、库选择和公理审计仍需要人类负责，而复杂证明对上下文、搜索预算和领域知识的要求，也远高于“证明偶数平方仍为偶数”这类演示任务。

MathCode 长期价值取决于能否把一次成功证明沉淀为下一次任务可复用的能力。如果 TheoremLib、Skills、Blueprint 和知识图谱能够随着使用持续增长，它获得的就不只是更长的对话历史，而是一套真正可积累、可检查、可协作的数学工程资产。

在 Coding Agent 普遍争夺软件仓库之后，MathCode 展示了下一块值得投入的领域：任何拥有严格语言、可执行反馈和明确验证器的知识工作，都可能被 Agent 重新组织。形式化数学只是其中最苛刻、也最能检验 Agent 是否真的会推理的一块试验场。

参考来源

• MathCode GitHub 仓库：项目源代码、安装说明、功能列表、支持平台及版本更新信息。