MathCode：让 AI 会做数学题的前沿代码智能体

当数学家遇上 AI 编程助手

想象这样一个场景：你是一名数学研究员，正在攻克一道组合数论难题。传统做法是翻阅厚重的手册、在 Lean 4 证明助手上手动一条条写证明——光是环境配置就可能花掉半天。现在，你只需要向 MathCode 描述你的问题，它就能自动生成完整的 Lean 4 形式化证明。

MathCode 是由 math-ai-org 团队开发的一个前沿数学代码智能体（Mathematical Coding Agent），核心能力是用 AI 自动生成 Lean 4 形式化数学证明。它将 GPT-5 等大模型的代码生成能力与 Lean 4 证明助手的形式化验证能力结合，专门解决"让 AI 真正理解和证明数学定理"这一难题。

图1：MathCode 工作界面，左侧为问题输入，右侧为生成的 Lean 4 证明代码

背景：形式化数学的困境与机遇

数学证明长期以来依赖人类数学家的严密推理，而形式化证明（Formal Proof）—— 即用计算机可验证的方式表述数学——始终是学术界的圣杯目标。Lean 4 是微软研究院推出的下一代证明助手，其数学库 mathlib 已成为全球数学家协作共享的重要基础设施，涵盖代数、拓扑、数论等数十个数学分支、数万个定理。

然而，Lean 4 的使用门槛极高：研究者必须同时精通数学和 Lean 4 语法，任何语法错误或逻辑漏洞都会导致证明失败。这严重限制了形式化数学的普及。MathCode 的出现正是为了打破这一瓶颈——它让 AI 充当"数学编程助手"，理解自然语言数学问题，自动生成可运行的 Lean 4 证明代码。

核心架构：多阶段推理工作流

MathCode 采用多阶段多智能体协作架构，每个阶段由专门的子模块负责，阶段之间通过状态传递形成完整的证明生成管道：

阶段一：问题理解与规划（Formalize Plan）

收到自然语言数学问题后，MathCode 首先调用 Codex（基于 GPT-5）进行深度推理，将问题拆解为若干子目标，生成结构化的"形式化计划"。这一阶段决定整个证明的逻辑走向——是采用归纳法、构造性证明还是反证法。

阶段二：代码生成（Formalize Code）

基于形式化计划，MathCode 调用代码生成模块生成 Lean 4 代码片段。它利用 mathlib 的定理库，通过检索相关已有定理（via lib_search 工具）避免重复造轮子。生成过程受严格的上下文限制，确保代码符合 Lean 4 语法规范。

阶段三：证明执行与验证（Prove）

生成的 Lean 4 代码被传入 Lean 4 编译器执行。如果编译失败，MathCode 会分析错误信息，调用 sorry_analyzer 定位未完成证明位置，通过 axiom_checker 排除非法公理引入，然后让 AI 重新生成——这形成了一个自我纠错循环。

阶段四：结果评估（Eval）

即使证明编译通过，MathCode 还会进一步评估证明质量：统计证明中的战术（Tactic）使用情况、识别潜在的冗余步骤、量化证明复杂度。proof_stats 工具提供详细的证明统计报告，帮助用户理解 AI 生成的证明是否优雅高效。

工具生态：五大专用工具模块

MathCode 的 tools/ 目录包含五个精心设计的 Python 工具，每个工具对应一个特定能力：

工具	文件	核心功能
axiom_checker	axiom_checker.py	检测非法公理引入，确保证明的数学纯粹性
lib_search	lib_search.py	检索 mathlib 已有定理库，为新证明提供素材
proof_stats	proof_stats.py	统计证明复杂度、战术使用、文件导入依赖
sorry_analyzer	sorry_analyzer.py	定位未完成的 sorry/admit 占位符
_lean_masking	_lean_masking.py	预处理 Lean 4 源码，辅助正则匹配

这些工具以标准化 JSON 格式输入/输出，方便与 AI 模型集成，是 MathCode 区别于通用代码生成工具的关键差异化组件。

后端路由：灵活的多模型架构

MathCode 在 AI 模型层面采用了灵活的路由策略，支持三种后端模式：

模式一（默认）：OpenAI Codex OAuth — 通过 codex auth login 认证，使用 OpenAI Codex（底层 GPT-5）作为所有推理阶段的引擎。配置简单，适合快速上手。

模式二：OpenRouter + 多模型路由 — 通过 OpenRouter API 接入多种模型（如 GPT-5.5、DeepSeek-V4、Gemini 3 Flash），支持按阶段配置不同模型：规划阶段用强推理模型，生成阶段用性价比模型，从而在效果和成本间取得平衡。

模式三：Anthropic 后端 — 切换到 Claude 系列模型，适合对 Anthropic 模型有偏好的用户。

.env.example 中详细定义了每种模式的配置变量，包括 OpenRouter 的 base URL、API Key、模型选择和推理预算参数。

部署方式：本地编译 + Web UI

MathCode 提供两种交互方式：

命令行模式：运行 bash run <problem> 直接处理数学问题。setup.sh 负责安装 Lean 4 工具链（通过 Elan 本地管理器）、下载 mathlib 依赖（8GB+缓存），安装完成后用户通过 .env 配置 API Key 即可。

Web UI 模式：运行 bash run webui 启动本地 Web 界面（index.html + mathcode-webui 二进制），提供更友好的交互体验，适合不熟悉命令行的用户。

注意：项目本身是 Shell 脚本包装器，Language 字段显示为 "Shell"。核心逻辑由预编译的 Rust/其他二进制（bin/ 目录）提供，Python 工具脚本负责辅助分析任务。

技术栈总结

MathCode 的技术栈组合非常独特：Shell 脚本作为入口和协调层，Python 工具处理形式化分析任务，而核心推理引擎来自 OpenAI Codex 或其他 LLM API。Lean 4 编译器（通过 Elan 本地安装）负责证明执行和验证。这种"脚本编排 + AI 推理 + 形式化验证"的三层架构，使其成为一个真正解决数学问题的专用系统，而非通用代码补全工具。

代码质量方面，Python 工具脚本遵循标准结构（docstring 规范、类型注解、命令行参数解析），证明分析工具使用正则表达式精确解析 Lean 4 语法树。setup.sh 体现了 DevOps 思维：支持幂等安装、本地工具链隔离（Elan HOME 控制在项目 .local/ 目录）、环境变量模板化。

局限与挑战

MathCode 并非银弹，存在几个重要局限：

证明生成的不确定性：大模型生成的证明可能在逻辑上正确但语义上不精确，或者恰好通过编译器但实际上依赖了"隐式公理"。axiom_checker 的存在本身就说明了这是一个需要严肃对待的风险。

对 mathlib 质量的依赖：MathCode 的能力上限受限于 mathlib 的定理覆盖范围。如果一个问题涉及的领域尚未被形式化，AI 能检索到的相关定理就非常有限。

部署复杂度：不提供 Docker 支持，用户必须手动安装 Lean 4 工具链、处理 Elan 环境变量、配置 API Key。对非 CS 背景的数学研究者有一定技术门槛。

无 Linux 二进制分发：虽然 bin/ 目录存在，但不含预编译二进制（size=0），用户必须从源码编译或依赖 setup.sh 下载预构建版本。

行业意义：数学 AI 的重要里程碑

MathCode 代表了 AI for Mathematics 领域的一个重要方向——不是让 AI 做题（计算），而是让 AI 证明（推理）。与传统依赖搜索-匹配的数学求解器不同，MathCode 的多阶段工作流试图在"理解问题 → 规划证明 → 生成代码 → 验证结果"这一完整链条上借助 LLM 的泛化能力。

从工程视角看，MathCode 的工具链设计（axiom_checker、lib_search、proof_stats 等）是教科书级别的多工具 Agent 实践。每个工具职责单一、接口标准化、输出 JSON 化，为未来扩展更多工具（如证明复杂度评估、自动证明重写）奠定了良好基础。

该项目目前 575 stars，在 math-ai 这个新兴细分领域属于较高关注度。随着 LLM 推理能力的持续提升和 mathlib 的不断壮大，形式化数学证明的自动化程度有望进一步提高，MathCode 的架构为此提供了一个有价值的实验平台。