MathCode, 数学编码代理

# MathCode — 前沿数学编程代理 来源：https://math-ai-org.github.io/mathcode/ ## 概述 MathCode 是一个终端 AI 编程助手，内置数学形式化引擎。向它提出自然语言描述的数学问题，它将自动转换为 **Lean 4** 定理并尝试形式化证明——具备持久化 Lean REPL、可复用定理与公理库、代理式证明能力，并集成 Obsidian 知识图谱。 MathCode 演示 ## 快速开始 需要 macOS（arm64）或 Linux（x86_64）系统，并需安装默认后端对应的 `codex` 命令行工具。 ```bash git clone https://github.com/math-ai-org/mathcode.git cd mathcode bash setup.sh codex auth login mathcode ``` `setup.sh` 脚本将准备发布版本目录、下载捆绑的运行时环境和 Lean 工具链，并安装用户本地的 `mathcode` 启动器。可通过以下命令试用： ```bash mathcode -p "prove that the square of an even number is even" ``` 输出结果保存至 `LeanFormalizations/` 目录。可通过 `\./run webui` 启动浏览器界面。 ## 功能特性 **持久化 Lean REPL** 通过持久化 Lean 语言服务器，单次预热后编译检查时间缩短至约 **0.4 秒**（原需约 30 秒）。 **定理库** 每个已证明的定理会自动命名、存储并支持导入，供证明器和规划器重复使用。 **公理库** 将对话中产生的假设存储为持久化、经过编译检查与一致性审查的 Lean 声明。 **Lean LSP 集成** 搜索 leansearch.net 和 Loogle 中经过验证的 Mathlib 引理，并利用结构化 LSP 诊断信息进行修正。 **Obsidian 定理图谱** 生成 Obsidian 知识库，将定理与引理的依赖关系可视化呈现为知识图谱。 **代理式证明** 每次证明过程转化为交互式会话，代理程序将编写候选证明、读取错误信息并重新编译。 **子目标树** 将复杂定理分解为独立的子目标并行证明，最后整合完整证明。 **多规划器** 并行运行多个规划器以生成多样化证明策略；证明器将选择最佳方案。 ## 引用说明 若在研究中使用 MathCode，请引用： ```bibtex @misc{mathcode2026, title = {MathCode: A Frontier Mathematical Coding Agent}, author = {Team Math-AI}, journal = {math-ai-org.github.io}, year = {2026}, month = {April}, url = {https://github.com/math-ai-org/mathcode} } ``` 数学形式化与证明流程基于 [AUTOLEAN](https://github.com/T3S1AMAX/autolean.git) 项目构建。