MathCode: An AI Coding Agent That Proves Math Theorems in Lean 4
MathCode, Mathematical Coding Agent
MathCode is a terminal-based AI coding assistant that turns plain-language math problems into formal Lean 4 theorems and proofs. It features a persistent Lean REPL for fast compile checks, a theorem library for reuse, an axiom store, and an Obsidian knowledge graph. The agent can prove theorems interactively, decompose complex goals into parallel subgoals, and use multiple planning strategies. It requires macOS or Linux and the codex CLI.
A persistent Lean language server brings compile checks to ~0.4s after a one-time warmup, instead of ~30s.