MathCode, Mathematical Coding Agent

# MathCode — A Frontier Mathematical Coding Agent Source: [https://math-ai-org.github.io/mathcode/](https://math-ai-org.github.io/mathcode/) ## Overview 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\.  ## Quick Start 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`\. ## Features **Persistent Lean REPL** A persistent Lean language server brings compile checks to**~0\.4s**after a one\-time warmup, instead of ~30s\. **Theorem Library** Every proved theorem is auto\-named, stored, and made importable so the prover and planner can reuse it\. **Axiom Library** Store conversational assumptions as persistent, compile\-checked, consistency\-reviewed Lean declarations\. **Lean LSP Integration** Searches leansearch\.net and Loogle for verified Mathlib lemmas and uses structured LSP diagnostics for repairs\. **Obsidian Theorem Graph** Generates an Obsidian vault that visualizes theorem\-to\-lemma dependencies as a knowledge graph\. **Agent\-Mode Proving** Each proof becomes an interactive session where the agent writes candidates, reads errors, and recompiles\. **Tree\-of\-Subgoals** Decomposes complex theorems into independent subgoals and proves them in parallel, then stitches them back\. **Multi\-Planner** Runs multiple planners in parallel for diverse proof strategies; the prover picks the best approach\. ## Citation 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} } ``` The math formalization and proving pipeline is based on the[AUTOLEAN](https://github.com/T3S1AMAX/autolean.git)project\.