MathCode — A Frontier Mathematical Coding Agent

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 REPLA persistent Lean language server brings compile checks to ~0.4s after a one-time warmup, instead of ~30s. Theorem LibraryEvery proved theorem is auto-named, stored, and made importable so the prover and planner can reuse it. Axiom LibraryStore conversational assumptions as persistent, compile-checked, consistency-reviewed Lean declarations. Lean LSP IntegrationSearches leansearch.net and Loogle for verified Mathlib lemmas and uses structured LSP diagnostics for repairs. Obsidian Theorem GraphGenerates an Obsidian vault that visualizes theorem-to-lemma dependencies as a knowledge graph. Agent-Mode ProvingEach proof becomes an interactive session where the agent writes candidates, reads errors, and recompiles. Tree-of-SubgoalsDecomposes complex theorems into independent subgoals and proves them in parallel, then stitches them back. Multi-PlannerRuns multiple planners in parallel for diverse proof strategies; the prover picks the best approach.