pi-lean4

Lean 4 theorem proving for the pi coding agent: eight tools over one Lean language server per session, proof-workflow skills, an unattended autoprove loop, and git guardrails.

• Tools — goals, diagnostics, tactic attempts on scratch copies, lemma search (local and four remote services), axiom and sorry checks, lake build, profiling and golf candidates.
• Skills — lean4 (the essentials), lean4-prove, lean4-repair, lean4-golf, lean4-formalize, lean4-review, with ~7k lines of reference material.
• Prompt templates — /lean-prove, /lean-repair, /lean-golf, /lean-review, /lean-checkpoint, /lean-formalize, /lean-disprove.
• /lean — server status and control, lake build, and /lean autoprove <file>.
• Hooks — every edit/write of a .lean file comes back with a compact compile check; destructive git commands are blocked inside Lean projects.

It ports the functionality of lean-lsp-mcp and lean4-skills (both MIT) to a native pi extension: TypeScript, no MCP, no Python.

Install

pi install npm:@ocramz/pi-lean4

Requirements: Node 24, pi, a Lean 4 Lake project, and lake on PATH or in ~/.elan/bin (install elan). ripgrep is needed for local search (pi's own copy is used if present). Linux and macOS.

From a checkout: pi -e ./pi-lean4 loads the extension with its skills and templates.

Tools

| Tool | What it answers | |------|-----------------| | lean_goal {path, line, column?, kind?} | the goals before/after a line, or at a point; kind: "term" for the expected type | | lean_diagnostics {path, startLine?, endLine?, declaration?, severity?, timeout?} | errors, warnings, sorries (tagged), with hints; partial results while elaborating | | lean_attempt {op: "tactics", path, line, snippets} / {op: "code", code} | try candidates on a scratch copy — "closes the goal", "goals remain", "fails"; or check standalone code | | lean_search {source, query} | local (project, packages, Lean core), leansearch, leanfinder, loogle, premises | | lean_nav {op, path, …} | hover, completions, definition, references, code actions (reported, not applied), outline | | lean_verify {op: "axioms" \| "sorries", …} | axiom dependencies classified standard/incomplete/native/custom; every sorry lexically | | lean_build {clean?, fetchCache?, force?} | lake build, skipped when nothing changed since the last success | | lean_analyze {op: "profile" \| "hypotheses" \| "golf", …} | per-line timing, unneeded hypotheses (report only), golf candidates |

Positions are 1-indexed lines and character columns. Failures (no project, no lake, bad parameters, rate limits) are error results; Lean's verdicts are normal results. The full reference the model reads is skills/lean4/references/tools.md.

The Lean server

• One per session, started lazily. Nothing runs until a tool needs Lean. A call about a file in another Lake project moves the server there. Concurrent first calls share one start.
• Stopped with the session. session_shutdown stops it for every reason (quit, /new, /resume, /fork, /reload): LSP shutdown, then the process group, then any worker that runs in a group of its own (Lean's workers do). If pi exits without that event, a process-exit hook kills what is left.
• Compiles only what a question needs. Files open with dependencyBuildMode: "never"; text is re-sent only when the bytes on disk changed; the "elaboration done" barrier is cached per version. When a file's imports are stale — Lean says so, or an in-project import changed on disk, which Lean does not notice by itself — the file is reopened once with "once", which rebuilds exactly its imports. lake build runs only through lean_build, and not even then if nothing changed.
• Throwaway text never touches disk. Tactic attempts, standalone code and axiom checks use scratch documents that exist only in the server.
• Crashes are noticed. Lean says nothing when a file worker dies; the client watches the process tree, reopens the file, and fails a waiting call promptly instead of at its timeout. More than three server crashes a minute stops the restarts.

/lean status shows where lake and rg were found, the setup check below, the project, the server and its open files, the build state, and the configuration. /lean restart / /lean stop replace or stop the server.

Setup check

When a session starts inside a Lake project (or above one), pi-lean4 checks the machine — file lookups only, nothing spawned, no network — and reports each problem with what it breaks and the commands that fix it:

| Finding | Severity | |---------|----------| | lake not found, or PI_LEAN_LAKE / lean4.lake points at nothing | error | | lake found in ~/.elan/bin but not on PATH (bash lake … commands will fail) | warning | | the project's pinned toolchain not installed (downloaded on first use) — an error in offline mode | warning | | Lean older than 4.24; lake not managed by elan (pin not enforced) | warning | | dependencies unresolved or not downloaded; Mathlib's build files missing (would compile Mathlib from source) | warning (error offline) | | ripgrep not found (local search only) | warning | | .lean files but no Lake project | warning | | .pi/settings.json lean4 settings ignored in an untrusted project | info |

The human sees the report on startup and /reload (a notification, or stderr in print mode) and a footer badge until it is fixed. The model is told before its first turn — what is broken, the fix, to ask before running a fix itself, and not to retry — and told again when the set of problems changes, including when they are resolved. A tool that fails for one of these reasons repeats the same fix in its error. Nothing needs a restart to pick up a fix, except adding a directory to PATH for bash.

Auto-check

After edit or write on a .lean file of the project the server is bound to, the result gets a line such as [lean auto-check] Foo.lean: compiles — no errors, no sorries. or the error count with the first errors. It waits at most autoCheckTimeoutMs and reports "still elaborating" past that. Mode running (default) never starts a server for this; always does; off disables it.

/lean autoprove

/lean autoprove <file> [--max-cycles=20] [--max-stuck=3] [--max-runtime=120m] runs the lean4-prove skill's cycle without asking, one cycle per turn. After every turn the extension itself measures the file (sorries and errors) and continues, or stops on: completion, the cycle budget, too many cycles in a row without progress, the running-time budget, Esc or a new prompt, or a failed model request. State is saved in the session: after /resume or /reload a loop comes back paused; /lean autoprove resume continues it, /lean stop-autoprove ends it.

Headless: pi -p "/lean autoprove Foo.lean" runs to the end and exits.

Git guardrails

Inside a Lean project (an ancestor has lean-toolchain or a lakefile), bash commands that would destroy uncommitted proof work are blocked: git reset --hard, git clean -f, whole-worktree checkout/restore, forced checkout/switch, and force/mirror/delete pushes. The command is parsed like a shell would (quotes, &&/;/|, $(…), bash -c, heredocs), so git commit -m "reset --hard" passes and cd x && git reset --hard does not. There is no bypass token; the human can run the command or use /lean guardrails off.

Remote search and privacy

lean_search sources other than local send the query — for premises, the goal text — to third-party services: leansearch.net, Lean Finder, loogle and leanpremise.net. They are rate-limited client-side as lean-lsp-mcp does (90, 10, 3 and 6 per 30 s). --lean-offline or PI_LEAN_OFFLINE=1 turns them off, along with Mathlib cache downloads and elan toolchain downloads. (Lake may still fetch missing package dependencies on its own.)

Configuration

First match wins: the --lean-offline flag, environment variables, then the lean4 key of the project's .pi/settings.json (read only for trusted projects), then defaults.

| Setting | Environment | Default | |---------|-------------|---------| | offline | PI_LEAN_OFFLINE | false | | autoCheck | PI_LEAN_AUTOCHECK | running (off, always) | | autoCheckTimeoutMs | PI_LEAN_AUTOCHECK_TIMEOUT_MS | 15000 | | guardrails | PI_LEAN_GUARDRAILS | true | | maxOpenFiles | PI_LEAN_MAX_OPEN_FILES | 4 (each is a Lean worker; with Mathlib, GBs) | | scratchSlots | PI_LEAN_SCRATCH_SLOTS | 1 | | maxOutputChars | PI_LEAN_MAX_OUTPUT_CHARS | 6000 per field (0 = unbounded) | | requestTimeoutMs / elaborationTimeoutMs / startTimeoutMs / buildTimeoutMs | PI_LEAN_*_TIMEOUT_MS | 2 min / 10 min / 2 min / 1 h | | lake, rg | PI_LEAN_LAKE, PI_LEAN_RG | found on PATH, ~/.elan/bin, pi's bin/, ~/.local/bin | | autoprove.maxCycles / maxStuckCycles / maxRuntimeMinutes | PI_LEAN_AUTOPROVE_MAX_CYCLES / _MAX_STUCK / _MAX_RUNTIME_MINUTES | 20 / 3 / 120 | | search.leansearchUrl / loogleUrl / leanfinderUrl / premiseUrl | PI_LEAN_LEANSEARCH_URL / … | the public services (a custom URL is not rate-limited) |

{ "lean4": { "autoCheck": "always", "maxOpenFiles": 2, "offline": true } }

Development

| Tier | Command | Needs | Covers | |------|---------|-------|--------| | unit | npm test | node | LSP framing/connection, positions, the server against a scripted fake LSP (process groups, stale imports, crashes), every op's text processing, search parsers with a stubbed fetch, guardrails, the autoprove state machine, the skills and templates | | types | npm run typecheck | — | everything against pi's real declarations | | interactive | npm run test:tui | pi, script | what the model is told (tools, guidelines, skills — snapshot: PI_UPDATE_PROMPT=1 to re-record), /lean, templates, guardrails, behaviour with no Lean | | Lean | npm run test:lean | pi, the pinned toolchain | Lean's behaviour the design relies on (contract.test.ts), every op on a real server, the lifecycle through pi -p with a scripted model, /lean autoprove headless, and one paid live case | | container | npm run test:container | podman | the unit suites and the extension in the pinned distroless image, with no Lean |

NB: The Lean tier runs on the host. From the repository root: make lean-install (elan, the toolchain pinned in shared/versions.env, ripgrep — into $HOME, no sudo), then make test-lean PKG=pi-lean4. The live case of the Lean tier needs OPENROUTER_API_KEY and fails without it.

Layout: src/ is plain TypeScript with no pi imports (the LSP client in src/lsp/, the server and runtime in src/lean/, one module per op in src/ops/, the hooks' logic in src/hooks/); extensions/ is the pi wiring; skills/ and prompts/ ship as package resources.

Credits

The tool behaviour, search backends and verification logic follow lean-lsp-mcp (© 2025 Oliver Dressler); the skills, references, guardrail rules and autoprove budgets follow lean4-skills (© 2025 Lean 4 Theorem Proving Skill Contributors). Both MIT; see THIRD_PARTY_NOTICES.md for details and a map of what derives from what. If you use the Lean API search services in research, cite their respective authors.