math-ai-org/mathcode

MathCode – AI‑powered Lean coding assistant

What it is – MathCode is a terminal‑based AI coding agent that helps you write, inspect, and verify formal proofs in the Lean theorem‑proving language. It bundles a Lean toolchain, a small web UI, and a set of “skills” that let the model interact with Lean (searching declarations, checking candidates, verifying proofs, etc.).

Key capabilities

• Goal‑driven proof writing – give the agent a natural‑language objective (e.g., “prove that the square of an even number is even”) and it will iteratively generate Lean code, call Lean tools, and refine the proof.
• Lean back‑ends – the agent can use an in‑process Lean REPL, a pinned subprocess, or an external Kimina Lean server for compilation and checking.
• Persistent libraries – you can store proved theorems (/theorem-store) and conversational axioms (/axiomatize) in a version‑controlled vault that the agent can later reuse.
• Obsidian graph export – generate a visual knowledge‑graph of theorem dependencies that can be opened in Obsidian.
• Web UI – a lightweight browser interface (./run webui) that runs a local daemon and shows the same interactive session as the terminal.
• Scheduling – slash commands like /loop 10m … let you set recurring prompts for reminders or periodic checks.

Installation & setup

1. Clone the repo and run bash setup.sh. The script:
   • Downloads a pre‑built runtime bundle (mathcode‑vX.Y.Z‑<os>-<arch>.tar.gz) if needed.
   • Verifies the download with SHA‑256 checksums.
   • Installs a user‑local launcher (~/.local/bin/mathcode).
   • Sets up a bundled Lean toolchain (.local/elan) and a cached Mathlib snapshot.
2. On Linux you must have bubblewrap (bwrap) and socat; on macOS the bundle works out‑of‑the‑box.
3. Optionally install the codex CLI if you want to use the default OpenAI‑backed model.

Typical workflow

# start an interactive session
mathcode -p "prove that the square of an even number is even"
# or pipe input
echo "hello" | mathcode -p

# launch the web UI
./run webui

Inside the session you can use slash commands:

• /goal <budget> <objective> – set a token budget and ask the agent to work on a proof.
• /theorem-store …, /axiomatize … – manage persistent theorem/axiom libraries.
• /obsidian generate – refresh the Obsidian graph.
• /loop … – schedule recurring prompts.

Configuration knobs (environment variables) let you tune the system, for example:

• MATHCODE_GOAL_MAX_TOKEN_BUDGET – caps the token budget for a goal.
• MATHCODE_MAX_CHAINED_COMMAND_INPUTS – limits how many nested tool calls the agent can make.
• MATHCODE_LEAN_REPL – forces the in‑process REPL.
• MATHCODE_KIMINA_SERVER and related vars – point to an external Kimina Lean server.

Maintenance

• bash setup.sh --status checks that the binaries, checksums, and bundled ripgrep are healthy.
• bash setup.sh --clean removes install artifacts while preserving your proof vault and Lean formalizations.

Who it’s for – Researchers, students, or developers who work with Lean and want an AI‑driven assistant to speed up theorem proving, explore Mathlib, and keep a reusable library of formal results.

---

All details above are taken directly from the repository’s README; no additional features have been inferred.