MathCode, Mathematical Coding Agent
MathCode is a new terminal-based AI coding assistant that integrates a math formalization engine to convert plain language problems into Lean 4 theorems. It features a persistent REPL, automated proof planning, and an Obsidian-based knowledge graph for visualizing theorem dependencies.
Why it matters
This tool bridges the gap between natural language AI and formal mathematical verification, potentially accelerating research and reducing errors in complex mathematical proofs.
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.
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 .
A persistent Lean language server brings compile checks to ~0.4s after a one-time warmup, instead of ~30s.
Get smarter about the news
Sign up free for a feed built around what you actually care about, Dive Deeper research on any story, and the full text of every article.
Create free accountAlready have an account? Sign in