MathCode — A Frontier Mathematical Coding Agent

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

Latest release: MathCode v0.3.0. 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

Explicit theorem-store actions compile, mirror, and index reusable declarations without hidden persistence.

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-Directed Proving

The agent writes candidates, inspects goals and diagnostics, and decides what to try next.

Optional Subgoal Exploration

Subgoals, helper lemmas, branches, and milestones are available as techniques, never a mandatory controller.

Strict Lean Verification

A fresh final check verifies one declaration; only a successful verification certificate counts as completion.

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}
}

MathCode preserves useful proof-search ideas as optional agent guidance while Lean remains the proof authority.