Skip to content

LeanProbe 0.3.1

Choose a tag to compare

View all tags
@Lemmy00 Lemmy00 released this 18 Jun 20:07
· 6 commits to main since this release
v0.3.1
a9adea4

LeanProbe 0.3.1

Fast Lean 4 proof feedback for AI agents — an MCP server, CLI, and Python API,
built on LeanInteract. It keeps a Lean REPL warm and reuses the elaborated
environment, so repeated checks return in tens of milliseconds instead of the
seconds a fresh lake build costs (~9–14× faster for sequential same-file work).
It never edits files; lake build stays the final whole-project gate.

Install (MCP server now included)

pip install lean-probe          # or: uvx lean-probe mcp
claude mcp add lean-probe --env LEAN_PROBE_AUTO_BUILD=0 -- lean-probe mcp

Works with Claude Code, Codex, and any MCP client (config snippets in the README).

What it gives an agent:

  • lean_check — verify any standalone snippet (the default; no file/name needed).
  • lean_check_target — check or replace a declaration in a project file against its warm prior environment (sub-second after the first call).
  • lean_proof_state / lean_tactic / lean_close_proof — drive a sorry tactic by tactic.
  • Agent-first: ships usage instructions on connect, actionable error_code + hint
    on every failure, and a compact inline feedback_lean for the next attempt.

Since 0.3.0

  • mcp is now a core dependency — pip install lean-probe ships the server (no extra).
  • Renamed AGENT.md → AGENTS.md (using-the-tool contract + contributor guide).
  • Quickstart-first README with copy-paste setup for Claude Code, Codex, and generic clients.

0.3.0 was the agent-usability redesign: server instructions, the lean_* tool set
with the low-friction lean_check, a guarded replacement, env-aware REPL recovery,
and the compact feedback_lean. Full notes in CHANGELOG.md.

Assets 2
Loading