math-ai-org/mathcode

MathCode – 基于 AI 的 Lean 编码助手

是什么 – MathCode 是一个基于终端的 AI 编码代理，帮助您在 Lean 定理证明语言中编写、检查和验证形式化证明。它捆绑了 Lean 工具链、一个轻量级 Web UI，以及一组“技能”，使模型能够与 Lean 交互（搜索声明、检查候选、验证证明等）。

核心功能

• 目标驱动的证明编写 – 提供自然语言目标（例如：“证明偶数的平方是偶数”），代理将迭代生成 Lean 代码，调用 Lean 工具，并优化证明。
• Lean 后端 – 代理可以使用进程内 Lean REPL、固定子进程或外部 Kimina Lean 服务器进行编译和检查。
• 持久化库 – 您可以将已证明的定理（/theorem-store）和对话式公理（/axiomatize）存储在版本控制的保险库中，供代理后续重用。
• Obsidian 图谱导出 – 生成定理依赖关系的可视化知识图谱，可在 Obsidian 中打开。
• Web UI – 一个轻量级浏览器界面（./run webui），运行本地守护进程，并显示与终端相同的交互式会话。
• 调度 – 使用 /loop 10m … 等斜杠命令，可设置重复提示，用于提醒或周期性检查。

安装与设置

1. 克隆仓库并运行 bash setup.sh。该脚本：
   • 如需，下载预构建的运行时包（mathcode-vX.Y.Z-<os>-<arch>.tar.gz）。
   • 使用 SHA-256 校验和验证下载内容。
   • 安装用户本地启动器（~/.local/bin/mathcode）。
   • 设置捆绑的 Lean 工具链（.local/elan）和缓存的 Mathlib 快照。
2. Linux 上必须安装 bubblewrap（bwrap）和 socat；macOS 上该包可开箱即用。
3. 如需使用默认的 OpenAI 支持模型，可选择安装 codex CLI。

典型工作流

# 启动交互式会话
mathcode -p "prove that the square of an even number is even"
# 或通过管道输入
echo "hello" | mathcode -p

# 启动 Web UI
./run webui

在会话中可使用斜杠命令：

• /goal <budget> <objective> – 设置令牌预算并要求代理处理证明。
• /theorem-store …, /axiomatize … – 管理持久化定理/公理库。
• /obsidian generate – 刷新 Obsidian 图谱。
• /loop … – 设置重复提示。

配置选项（环境变量）可让您调整系统，例如：

• MATHCODE_GOAL_MAX_TOKEN_BUDGET – 限制目标的令牌预算上限。
• MATHCODE_MAX_CHAINED_COMMAND_INPUTS – 限制代理可执行的嵌套工具调用次数。
• MATHCODE_LEAN_REPL – 强制使用进程内 REPL。
• MATHCODE_KIMINA_SERVER 及相关变量 – 指向外部 Kimina Lean 服务器。

维护

• bash setup.sh --status 检查二进制文件、校验和以及捆绑的 ripgrep 是否健康。
• bash setup.sh --clean 删除安装产物，但保留您的证明库和 Lean 形式化内容。

适用人群 – 使用 Lean 并希望借助 AI 驱动的助手加速定理证明、探索 Mathlib 并维护可重用形式化结果库的研究人员、学生或开发者。

---

以上所有细节均直接取自仓库的 README；未推断任何额外功能。