MathCode 将以自然语言表述的问题转换为 Lean 4 定理，并尝试进行形式化证明

Why it matters

MathCode shows how AI math tools are shifting from one-off answers toward persistent, reusable proof libraries, with Lean's compiler providing a hard verification layer.

公开材料最明确地将 Yifan Zhang (@yifanzhang_) 与 Math-AI 联系起来，后者是支持 MathCode 的开放研究社区。MathCode 是一个终端 AI 编程助手，它将以普通语言书写的数学内容转换为 Lean 4 陈述，尝试形式化证明，并将成功结果保存以便日后使用。

MathCode 的项目页面 将该项目的时间标为 2026 年 4 月。应将 MathCode 视为一个持续的开源研究项目，而非一次新的发布。

这一区别很重要，因为 MathCode 最有力的理念超出了其初始发布：Zhang 的团队将形式化数学视为一个代码库，代理可以逐步扩展、搜索和重用。每一个成功的定理都可以成为下一个证明的基础设施。

Zhang 自称是 Princeton University 的博士生和 Princeton AI Lab Fellow，研究方向包括语言模型推理、强化学习、预训练和模型架构。他公开的研究组合包括数学文本的整理和推理系统，这些工作有助于解释 MathCode 强调将无结构的数学语言转化为持久的机器可读对象的原因。

Math-AI 将自己定位为一个开放研究社区，通过 GitHub 和 Hugging Face 发布代码、模型和研究材料。其公开材料并未将 MathCode 表述为商业服务，且该项目没有披露定价、收入或客户数据。

A proof assistant built like a coding agent

开源的 MathCode 存储库 将工作流打包为面向 macOS（Arm 处理器）和 Linux（x86_64 系统）的终端应用。用户可以提交诸如 “证明偶数的平方是偶数” 之类的提示。MathCode 将请求形式化为一个 Lean 定理，生成证明候选、编译它们，并利用 Lean 的错误信息来指导下一次尝试。

本地部署是一个有意的产品选择。MathCode 会安装捆绑的 Lean 工具链，维护一个持久的语言服务器，并将生成的工作写入 LeanFormalizations 目录。还包含浏览器界面，但终端仍是主要的工作流程。

默认路径依赖于 OpenAI 的 Codex CLI 及其认证系统。仓库同时记录了兼容 Anthropic 和兼容 OpenAI 的后端。该灵活性让研究人员对底层模型有一定控制，但 MathCode 的证明质量、延迟和运行成本仍在一定程度上取决于他们选择的外部模型提供商。

MathCode 的文档 表示其持久的 Lean 进程在预热后将编译检查时间降至大约 0.4 秒左右，而当 Lean 必须反复启动并加载其库时大约需要 30 秒。上述数据来自该项目，并非独立基准。该设计仍然针对一个具体的代理问题：长的反馈周期使迭代修复证明代价高昂，而持久的编译器允许模型快速失败并重试。

该代理可以将定理拆分为子目标， 并行运行多种规划策略，然后将成功的片段拼接成最终证明。它还会在 LeanSearch 和 Loogle 中搜索现有的 Mathlib 引理，并将结构化的编译器诊断反馈回证明循环。

MathCode 建立在 AUTOLEAN project 之上，后者提供了底层的形式化和证明流水线。Math-AI 的贡献在于周边的工作环境：持久状态、库搜索、迭代修复、并行规划以及用于保留代理已证明内容的接口。

Zhang is betting on memory, not disposable answers

最关键的特性是 MathCode 对既往工作的处理。成功编译的定理可以被自动命名、写入可重用的 Lean 库并在后续会话中导入。用户还可以将对话中的假设存储为经编译检查的公理声明。

这既带来效用，也带来风险。Lean 可以验证一个证明是否从其陈述的前提出发成立，但它无法保证用户的前提准确地描述了现实世界。MathCode 的文档称其包含用于已存储公理的一致性审查工具，但由此形成的知识库的可靠性仍然依赖于细致的规范和库管理。

MathCode 还会生成一个 Obsidian vault，用于映射定理和引理之间的依赖关系。该图谱是 Zhang 更广泛研究方向的一个实际表达：数学输出应累积成可导航的结构，而不是在聊天会话结束时消失。

这种方法赋予 MathCode 与托管问答系统不同的产品形态。当相同的研究人员持续使用它、整理定理并构建本地的形式知识库时，其价值会增长。这可能适用于希望获得可检查文件并控制工具链的证明工程师和有技术能力的数学家。安装要求和以 Lean 为中心的工作流缩小了最初的受众范围。

Formal mathematics is becoming an agent category

MathCode 进入的是一个有多支团队试图将语言模型与证明助理配对的领域。Harmonic's Aristotle 接受英文问题，生成 Lean 的形式化表示，并可以直接在现有的 Lean 仓库中工作。Harmonic 表示其托管代理最多可自主运行 24 小时。

Math Inc.'s Gauss 针对大型研究性形式化，依赖大量计算和人工数学指导。Math Inc. 还发布了 OpenGauss，这是一个带有公开评估框架的开源套件。Axiom Math's AXLE 以及包括 LeanDojo 在内的研究项目则覆盖证明生成与验证栈的其他部分。

MathCode 尚未发布独立的证明成功基准来证明其优于这些系统。其公开文档也未提供活跃用户数、推理开销或达到有效证明的自然语言问题比例等数据。

其无可争辩的贡献是 Zhang 与 Math-AI 围绕形式化证明所选择的开发者体验。MathCode 将编译器循环、定理记忆、公理管理、并行规划和依赖图整合到一个本地环境中。在它能够宣称广泛的数学可靠性之前，这种组合就已使其成为一个可检查的研究系统。

对 Zhang 而言，MathCode 将他工作的若干脉络连接起来：选择数学训练数据、改进推理系统，以及将形式化验证作为对模型输出的严格检验。该代码库为这些研究提供了一个人们可以运行、修改和审计的产品表面。接下来的检验是实证性的：积累的记忆是否真的能帮助用户完成困难的形式化工作，以及这些收益能否与日益强大的替代方案进行比较衡量。