Install · CLI · Benchmark · Config

Docs

An agent that writes Lean 4 proofs. Give it a theorem; it loops (LLM draft → lake build → parse diagnostics → repair) until the proof type-checks. Nothing counts as proved until Lean's kernel accepts it.

install

# 1. Lean toolchain + Mathlib (once) curl https://elan.lean-lang.org/elan-init.sh -sSf | sh cd lean && lake update && lake exe cache get && lake build # 2. Python deps pip install -e . pip install textual pyperclip

configure

# any OpenAI-compatible endpoint export OPENAI_API_KEY=... export OPENAI_BASE_URL=http://localhost:11434/v1 export PROVER_MODEL=gpt-4o # free: OpenCode Zen, e.g. big-pickle export OPENAI_BASE_URL=https://opencode.ai/zen/v1

prove

prover prove "theorem absl (a : ℤ) : a ≤ |a|" # best-of-N, full-file mode, adaptive steps prover prove "..." --n-attempts 3 --adaptive # script-friendly JSON on stdout prover ask "theorem x : True := by trivial"

benchmark

prover bench --max-steps 20 --report report.json --results benchmark-results.json # pure-Lean floor, no LLM prover lean-baseline --tactic prover_finish # record your score to the board prover leaderboard --run --name my-model

tui

prover # interactive TUI: browse problems, watch live repairs, # queue parallel workers, slash commands, themes # expose to Claude / opencode / Cursor prover mcp

config

# precedence: env > project > user > defaults PROVER_MAX_STEPS=20 ~/.prover/settings.json .prover/settings.json # per-tool allow/deny ACL /permissions remember allow lean_build

Full guide and architecture live in the repo: GUIDE.md · ARCHITECTURE.md