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.
- muds
Interesting work. Is this a wrapper around the AUTOLEAN project (https://github.com/T3S1AMAX/autolean)?
- eisbaw
the tricky bit is ensuring your inaccurate plain english statement is captured and formalized correctly as lean.
- owlbite
Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.