MathCode, Mathematical Coding Agent

MathCode, a terminal AI coding assistant with a built-in math formalization engine, automatically converts plain-language math problems into Lean 4 theorems and attempts formal proofs, featuring a persistent Lean REPL with compile checks in ~0.4 seconds after warmup, reusable theorem and axiom libraries, agentic proving, and an Obsidian knowledge graph. The open-source tool, released by Team Math-AI on GitHub, requires macOS (arm64) or Linux (x86_64) and the codex CLI, and is based on the AUTOLEAN project.

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. Overview 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.