MathCode 把自然语言题自动收成 Lean 证明

介绍 MathCode：终端数学编码 Agent，内置 Lean 4 形式化、持久 REPL、定理库与 Obsidian 依赖图，默认后端 Codex。

MathCode 把自然语言题自动收成 Lean 证明

MathCode 是 Show HN 上的终端数学编码助手：用白话描述题目，它转成 Lean 4 定理并尝试形式化证明。站点：MathCode，代码在 math-ai-org/mathcode。默认后端要装 codex CLI。

作者：CodePass 技术编辑

快速上手

需要 macOS arm64 或 Linux x86_64：

git clone https://github.com/math-ai-org/mathcode.git
cd mathcode
bash setup.sh
codex auth login
mathcode

setup.sh 会拉运行时与 Lean 工具链，并装用户级 mathcode 启动器。示例：mathcode -p "prove that the square of an even number is even"，产物进 LeanFormalizations/。也可用 ./run webui 开浏览器 UI。

和普通 coding agent 差在哪

持久 Lean REPL：预热后编译检查约 0.4s 量级（对比冷启动约 30s）。证过的定理入库可 import；对话里的假设可落成受一致性审查的 axiom。集成 leansearch / Loogle 与 LSP 诊断修错；可生成 Obsidian 金库画定理依赖图。证明过程支持 agent 循环、子目标树并行、多 planner 再选路。管线基于 AUTOLEAN 一类工作。

适合谁

形式化数学、需要可机检证明的研究原型。它不是通用 Web 开发 IDE。Codex 额度与 Lean 学习曲线仍是成本；先用官方示例题验证环境，再上论文级命题。