MathCode 把 Lean 装进终端 Agent：数学证明也开始有编码工作流
作者：林岚｜OC 开发者生态编辑
林岚
MathCode 发布一款面向数学形式化的终端 AI 助手。用户可以输入自然语言数学问题，工具将其转换成 Lean 4 定理，调用 Agent 尝试证明，并根据编译器返回的目标和错误继续修改。项目默认使用 Codex CLI 作为后端，也支持其他模型配置。
一句话结论：MathCode 借用 AI 编程工具的循环，把“写证明”改造成规格、编译、报错和修复的终端工作流，但能运行不等于已经证明它比数学家或现有证明器更强。
形式化数学过去最费时间的部分，往往不是想出证明思路，而是把自然语言定义准确翻译成 Lean、找到 Mathlib 中已有引理，并让每个类型和前提通过检查。MathCode 把这些步骤组织成 Agent 工具：搜索引理、写候选证明、读取结构化诊断，失败后最多多轮修复。
项目还提供定理库、经过一致性检查的公理库、Lean LSP 搜索和 Obsidian 依赖图。复杂问题可以拆成带 sorry 占位的子目标，交给多个规划器并行寻找路线，再把通过的部分拼回完整证明。这些功能更像软件工程中的代码索引、构建缓存和任务分解，而不是聊天机器人直接报出答案。
性能方面，项目方称持久 Lean 服务在约 90 秒预热后，可把后续编译检查从约 30 秒降到约 0.4 秒。这个数字来自项目自测，尚无独立基准，也会受 Mathlib 导入范围、机器和定理规模影响。当前预编译版本面向 macOS arm64 与 Linux x86_64。
更重要的边界是形式化对象本身。如果 Agent 把原题翻译错了，Lean 只能证明错误命题在其公理下成立。公理库虽然方便保存对话假设，也可能把未经审查的前提长期带入后续证明。人仍要审查定理陈述、假设和依赖，而不只是看最后是否编译通过。
关键事实
- 产品形态：终端 AI 助手，内置 Lean 4 形式化与编译反馈
- 默认后端：Codex CLI，可配置其他模型
- 工程能力：持久 Lean 服务、LSP 搜索、定理与公理库、子目标树和多规划器
- 证据边界：性能与能力主要来自项目方说明，缺少独立评测
OC 判断
MathCode 最值得观察的不是“AI 会不会做奥数”，而是数学证明是否会形成类似编码的可维护项目：有文件、有依赖、有编译错误、有可复用库，也有明确审查点。工具若能稳定减少形式化摩擦，就已经有价值；把编译成功包装成数学发现则还太早。
为什么重要
- 对数学研究者：自然语言到 Lean 的转换和引理搜索可能降低形式化门槛。
- 对开发者：证明 Agent 展示了编译器反馈如何约束模型，而不只依赖自我评价。
- 对教育用户：机器可检查证明有助于定位步骤错误，但不能替代对命题和假设的理解。
评论
围绕这篇文章补充信息、提出问题或分享观察。