# MathCode, Mathematical Coding Agent

> Source: <https://math-ai-org.github.io/mathcode/>
> Published: 2026-08-16 18:17:10+00:00

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.