🔶 MathCode：数学编程 Agent

英文标题：🔶 MathCode, Mathematical Coding Agent

MathCode 是一款面向数学形式化的编程 Agent，默认后端依赖 `codex` CLI。它目前要求运行在 macOS（arm64）或 Linux（x86_64）环境中，并通过安装脚本配置运行时与 Lean 工具链。开发者可通过自然语言提示生成证明，输出结果会写入 `LeanFormalizations/` 目录，也可启动浏览器 Web UI 使用。

打开原文相关 6 · 机会 1

中文

需要 macOS（arm64）或 Linux（x86_64），并且默认后端需要安装 codex CLI。

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。

English / 原文

Requires macOS (arm64) or Linux (x86_64), plus the codex CLI for the default backend.

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

setup.sh prepares the release checkout, downloads the bundled runtime and Lean toolchain, and installs a user-local mathcode launcher. Try it with:

mathcode -p "prove that the square of an even number is even"

Outputs are written to LeanFormalizations/. A browser UI is available via ./run webui.