MathCode is a terminal AI coding assistant with a built-in math formalization engine. Give it a math problem in plain language and it will automatically convert it into a Lean 4 theorem and attempt a formal proof — with a persistent Lean REPL, reusable theorem and axiom libraries, agentic proving, and an Obsidian knowledge graph.
Latest release: MathCode v0.4.0. Requires macOS (arm64) or glibc-based Linux (x86_64 with AVX2), 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
./runsetup.sh prepares the release checkout, downloads the bundled runtime, offers optional Lean/Mathlib installation, and installs a user-local mathcode launcher for new shells. Use --without-lean for a lightweight install, or --with-lean for the full toolchain. Try it with:
mathcode -p "prove that the square of an even number is even"The agent works directly in the selected workspace, and only a successful strict Lean verification certifies a finished proof. A browser UI is available via ./run webui.
Eligible checks can reuse an explicitly configured, project-matched Lean service; strict final verification always runs fresh.
Explicit theorem-store actions compile, mirror, and index reusable declarations without hidden persistence.
Store conversational assumptions as persistent, compile-checked, consistency-reviewed Lean declarations.
Searches leansearch.net and Loogle for verified Mathlib lemmas and uses structured LSP diagnostics for repairs.
Generates an Obsidian vault that visualizes theorem-to-lemma dependencies as a knowledge graph.
The agent writes candidates, inspects goals and diagnostics, and decides what to try next.
Subgoals, helper lemmas, branches, and milestones are available as techniques, never a mandatory controller.
A fresh final check verifies one declaration; only a successful verification certificate counts as completion.
Detailed guides for installation, everyday use, Lean proofs, and configuration. Available in English and Chinese.
If you use MathCode in research, please cite:
@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}
}MathCode preserves useful proof-search ideas as optional agent guidance while Lean remains the proof authority.