lean-prover

An agent that writes Lean 4 proofs. You give it a theorem; it iterates (LLM draft → lake compile → parse diagnostics → fix) until the proof type-checks. Ends with ∎

Status

Working agent, 100-problem benchmark, interactive TUI, MCP server, session resume/branching, history compaction, theming, best-of-N search, local Mathlib retrieval, autoformalization, synthetic data tooling. Current best: Qwen3.8-27B on Mathlib v4.20.0 scores 68/100 (trivial 20/20, easy 23/30, medium 21/30, hard 4/20), $0 cost (free HF endpoint). Public leaderboard: https://lean-prover.github.io/lean-prover/

Setup

# 1. Lean toolchain + Mathlib (once; Mathlib fetch takes a while)
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
source ~/.bashrc
cd lean && lake update && lake exe cache get && lake build && cd ..

# 2. Python deps
pip install -e .
pip install textual pyperclip   # for the TUI + clipboard
pip install pytest              # to run the test suite

# 3. LLM access (any OpenAI-compatible endpoint)
export OPENAI_API_KEY=...          # or
export OPENAI_BASE_URL=http://localhost:11434/v1  # e.g. Ollama
export PROVER_MODEL=gpt-4o

Environment variables

Variable	Default	Purpose
OPENAI_API_KEY / OPENAI_BASE_URL	—	Any OpenAI-compatible provider.
PROVER_MODEL	gpt-4o	Model name for /status + cost lookup.
PROVER_CONTEXT_WINDOW	per-model table in llm.py	Override the context-window size used to compute the auto-compaction budget.
PROVER_SESSIONS_DIR	~/.prover/sessions	Where proof sessions (JSONL) are recorded.
PROVER_PROMPTS_DIR	~/.prover/prompts (or $PROVER_CONFIG_DIR/prompts)	User-level prompt templates (project <repo>/.prover/prompts wins).
PROVER_THEMES_DIR	~/.prover/themes	Custom TUI themes (*.json).
PROVER_LOGS_DIR	~/.prover/logs	Diagnostic logs.
PROVER_CONFIG_DIR	~/.prover	Overrides the whole user config home (prompts/themes/logs/trust).
PROVER_TRUST	always	Project trust policy: always / never / ask.
PROVER_NO_SESSIONS	0	1 disables session recording.
PROVER_BRANCH_SUMMARY	1	0 disables model-assisted branch summaries.
PROVER_THINKING	unset (off)	Reasoning level: off/minimal/low/medium/high/xhigh. Non-off sends OpenAI reasoning_effort.
PROVER_DISABLE_THINKING	1	Hard thinking off-switch (vLLM/HF enable_thinking: False); an explicit PROVER_THINKING wins.
PROVER_LLM_TIMEOUT	180	Hard wall-clock cap (seconds) per LLM call.
PROVER_RETRIEVE	unset	1 enables local Mathlib lemma retrieval hints (keyword index over the pinned mathlib checkout, built lazily in lean/tmp/lemma_index.json).
PROVER_LEMMA_PLAN	unset	1 enables lemma-bank planning: propose ≤3 helper lemmas, prove them first, prepend only proven ones above the main theorem.
PROVER_MODEL_<TIER>	PROVER_MODEL	Per-difficulty model override (<TIER> = TRIVIAL/EASY/MEDIUM/HARD).
PROVER_TEMP_<TIER>	caller default	Per-difficulty sampling temperature (float).
PROVER_STEPS_<TIER>	caller default	Per-difficulty max repair steps (int).

Usage

# Prove a single theorem interactively (edits lean/src/Prover.lean)
prover prove "theorem pythagoras (a b c : ℕ) : a ^ 2 + b ^ 2 = c ^ 2 ↔ a = 0" --max-steps 20
prover prove "..." --n-attempts 3      # best-of-N (temperature ramp per attempt)

# Autoformalize a natural-language statement to a compilable Lean theorem
prover formalize "For all integers a and b, a + b = b + a."

# Generate a synthetic proof corpus (statement, proof, ok) as JSONL
prover synth-data --count 20 --out synth.jsonl   # train file: synth_train.jsonl (proven only)

# Import a standard benchmark (MiniF2F Lean4 port) + type-check it
python benchmark/import_standard.py minif2f --src <miniF2F-lean4 checkout> --split test --verify
prover bench --problems benchmark/minif2f_test.json

# Interactive TUI: browse problems, watch live repairs, slash commands
prover tui            # or: prover tui -p 4 (parallel workers)

# Slash commands inside the TUI prompt bar (Tab-less: ctrl+space completes):
#   /help /prove /run /stop /workers <n> /resume <id> /branch <id> [turn]
#   /export <path> /theme [name] /status /model /system /hotkeys /clear /quit
#   /usage [session-id|all] /reload

# Run the benchmark (100 theorems, JSON in benchmark/problems.json)
prover bench --max-steps 20 --report report.json
prover bench --parallel 4            # isolation makes parallelism safe
prover bench --no-goal-feedback      # errors only, no LSP goal state
prover bench --no-record             # skip JSONL session logs
prover bench --n-attempts 2          # best-of-N per problem

# Inspect recorded proof sessions (event stream per run)
prover sessions                      # list recent sessions
prover sessions 20260817-015954-proof       # replay one
prover sessions 20260817-015954-proof --raw # with raw JSON records

# Token/cost dashboard (per session or across all)
prover usage                         # all sessions
prover usage 20260817-015954-proof   # one session

# Machine-readable proof output
prover prove "..." --output json         # one JSON event per line
prover prove "..." --output transcript   # colored step transcript

# Local leaderboard: run a subset and record the score
prover leaderboard --run --problems benchmark/trivial.json --name my-model
prover leaderboard --show
# Public board: https://lean-prover.github.io/lean-prover/ (deploys via GitHub Pages on push)

# Use lean-prover from any MCP client (Claude, opencode, Cursor, …)
prover mcp    # JSON-RPC tools: prove_theorem, benchmark_score, problems

# Tests
pytest tests/        # ~292 tests (loop, compaction, session, TUI, commands)

How it works

        ┌────────────┐
        │ statement  │
        └─────┬──────┘
              ▼
   ┌─────────────────────┐
   │ hammer pre-pass     │  ring / omega / linarith / simp / …
   │ (before any LLM)    │  → most easy problems stop here
   └─────────┬───────────┘
             ▼ (no hammer worked)
   ┌─────────────────────┐
   │ LLM drafts/patches  │◄──────────────┐
   │ the proof body      │               │
   └─────────┬───────────┘               │
             ▼                           │
        ┌─────────────┐   diagnostics    │
        │ lake env    │   + goal state   │
        │ lean --check│──────────────────┘
        └─────┬───────┘   (LSP RPC, source context)
              ▼  type-checks
           [PROVED ∎]

The model only ever supplies the proof body — the theorem statement is assembled by us, so "prove a different theorem" is structurally impossible. History is compacted (old attempts folded into a failed-attempts summary) rather than truncated, so weak models stop re-trying dead ends.

Optional search/assistance layers (all env-gated, all default off, all best-effort — a failure never breaks the loop):

• Best-of-N (--n-attempts): independent repair trajectories with a temperature ramp; hammers run once (they are deterministic); returns the first proof, else the attempt that got furthest.
• Lemma retrieval (PROVER_RETRIEVE=1): keyword index over ~150k Mathlib lemma signatures; the top-5 for the target statement are fed to the model as hints (no embeddings, no network).
• Lemma planning (PROVER_LEMMA_PLAN=1): the model proposes ≤3 helper lemmas, each is statement-checked and proven by a bounded sub-loop, and only proven helpers are prepended above the main theorem (never sorry).
• Per-difficulty routing (PROVER_MODEL_<TIER> etc.): pick a cheaper model for trivial/easy and a stronger one for hard.

Layout

lean/               Lean 4 package (lake), Mathlib pinned to v4.20.0
  src/Prover.lean   target file the agent edits
  tmp/              per-problem files (benchmark isolation)
agent/              the agent (Python)
  loop.py           repair loop + hammer pre-pass + resume/branch
  events.py         event protocol — one stream to trace/session/TUI
  session.py        JSONL sessions (~/.prover/sessions/)
  session_manager.py index.jsonl upsert/list + history rebuild
  session_stats.py  per-session token + cost aggregation
  compaction.py     failed-attempts summary (tau's memory model)
  lean.py           lake invocation + diagnostic parsing
  llm.py            LLM provider (OpenAI-compatible) + cost tracking
  lsp.py            Lean language server client (goal-state feedback, run_tactic RPC)
  retrieval.py      local Mathlib lemma-signature keyword index + search
  router.py         per-difficulty model/temperature/step routing (env table)
  formalize.py      autoformalization (NL → compilable Lean theorem)
  plan.py           lemma-bank planning (prove helpers before the main theorem)
  synth.py          synthetic proof corpus generation (JSONL + train split)
  mcp.py            MCP server (expose prove_theorem to any agent)
  commands.py       slash-command registry (tau pattern, 22 built-ins)
  paths.py          canonical user/project dir config (env overrides)
  context_window.py token-based context estimation + auto-compaction threshold
  session_usage.py  /usage token + cost dashboard
  thinking.py       reasoning levels → provider kwargs (tau thinking port)
  diagnostics.py    structured JSONL failure log (~/.prover/logs/, tau port)
  rendering.py      --output text/json/transcript renderers (tau rendering port)
  autocomplete.py   slash-command completions (tau pattern)
  themes.py         TUI themes as JSON data (tau pattern)
  terminal_title.py OSC terminal title + braille spinner (tau pattern)
  tui.py            Textual TUI (problems, live trace, replay, commands)
  main.py           CLI (prove / bench / tui / mcp / sessions / usage / leaderboard)
benchmark/          fixed theorem set + runner + import_standard.py + merge_reports.py
tests/              pytest suite (317 tests)
leaderboard.json    local score history (prover leaderboard)
site/               public leaderboard site (GitHub Pages)

Roadmap

• 100-problem graded benchmark (benchmark/problems.json)
• Better error-context extraction (surrounding source, not just line:col)
• Per-problem Lean file isolation (parallel runs)
• Proof trace logging + cost tracking
• Goal-state feedback via Lean LSP (getInteractiveGoals)
• MCP server wrapper (prover mcp)
• Leaderboard (local: prover leaderboard; public site in site/)
• TUI: custom prove, session replay, parallel workers, Errors panel
• Clipboard (tau port: pyperclip + OSC-52 fallback, selection-aware)
• Slash commands + completions (tau pattern, 21 built-ins) + ctrl+k palette
• Session resume + branching (/branch <session> [turn], model branch summaries)
• File drops into the prompt bar (paths quoted/URI-decoded, tau port)
• Session export (/export, JSONL + self-contained HTML transcript)
• Project trust gating (.prover protected resources, modal + env policy)
• Prompt templates (/prompts picker, slash expansion, project override)
• History compaction (failed-attempts summary) + token-based auto-compaction
• Themes + terminal-title chrome + OSC 9/99 completion notification (tau pattern)
• Queued prompts while running (ctrl+e to edit), /new /compact /name (tau pattern)
• Session token + cost dashboard (/usage, per-session and across all)
• /reload resource change summary (problems/themes/prompts before→after)
• Thinking levels, structured failure log, --output renderers, prover usage CLI (tau port)
• Results post + public leaderboard (see leaderboard.json)
• Public leaderboard site (site/, GitHub Pages — updates on every push to leaderboard.json)
• Best-of-N search (--n-attempts, temperature ramp, first-proof-wins)
• Local Mathlib lemma retrieval (PROVER_RETRIEVE=1, ~150k-signature keyword index)
• Per-difficulty model/temperature/step routing (PROVER_MODEL_<TIER> table)
• Autoformalization (prover formalize, NL → compilable Lean, retry on diagnostics)
• Lemma-bank planning (PROVER_LEMMA_PLAN=1, proven-helpers-first)
• Synthetic data + expert-iteration corpus (prover synth-data)
• MiniF2F benchmark import + type-check (benchmark/import_standard.py)
• LSP runTactic primitive (RPC only present on Lean ≥ v4.22; returns None on our pinned v4.20 — verified against the real server)

Not yet verified / deferred (honest scope)

• Live-model verification of best-of-N, retrieval, planning, routing and formalize is blocked: the configured HF backup endpoint answers /models but hangs on /chat/completions (serverless queue stall). Unit tests pass; end-to-end model runs need a working endpoint.
• The runTactic RPC does not exist in the pinned Lean v4.20.0 toolchain (added in later Lean); the primitive is unit-tested and degrades to None.
• Full MiniF2F score (244 test problems) has not been run through the agent — the statements are type-checked (244/244 compile on Mathlib v4.20.0) but proving them is a long model run.
• Mathlib bump to current (grind tactic), real RL fine-tuning, and upstream contributions are explicitly out of scope (see PROPOSALS.md).