MathCode: A Mathematical Coding Agent with Lean 4 Formalization

MathCode is a terminal-based AI coding assistant that formalizes and proves math problems using Lean 4. Instead of writing Lean code yourself, you give it a problem in plain English, and it generates a theorem and attempts a proof, with a persistent REPL and a library of reusable theorems.

Key Features

• Persistent Lean REPL: After a one-time warmup, compile checks drop to ~0.4s (from ~30s).
• Theorem Library: Every proved theorem is auto-named, stored, and importable for reuse.
• Axiom Library: Store conversational assumptions as persistent, compile-checked Lean declarations.
• Lean LSP Integration: Searches leansearch.net and Loogle for verified Mathlib lemmas, uses structured LSP diagnostics for repairs.
• Obsidian Theorem Graph: Generates a visual dependency graph of theorems and lemmas in Obsidian.
• Agent-Mode Proving: Interactive sessions where the agent iterates on proof candidates based on errors.
• Tree-of-Subgoals: Decomposes complex theorems into independent subgoals, proves them in parallel, then stitches them together.
• Multi-Planner: Runs multiple planners in parallel for diverse proof strategies; the prover picks the best approach.

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

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.

This tool is aimed at mathematicians, researchers, and developers working with formal verification or AI-assisted theorem proving.