LeanProbe 0.4.0

• Split the agent contract out of AGENTS.md into an installable skill at
  src/lean_probe/skill/SKILL.md (YAML frontmatter + the MCP tool contract).
• New lean-probe install-skill drops it into agent clients' skills
  directories — ~/.claude/skills and ~/.codex/skills share the same
  skills/<name>/SKILL.md layout. Default installs to every present client
  ("both if both"); --client claude|codex forces one, --skills-dir PATH
  targets a root, --dry-run/--print preview. The skill ships inside the
  wheel, so pip install lean-probe && lean-probe install-skill needs no
  repo checkout.
• A plain pip install lean-probe stays skill-free — the skill is purely
  opt-in and a regular install writes nothing to ~/.claude/~/.codex.
• The README links to the skill as the single source of truth; a test keeps its
  tool table in sync with TOOL_NAMES.

LeanProbe 0.3.1

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.

LeanProbe 0.2.2

What's Changed

• Added lean_probe_capabilities MCP tool for reporting LeanProbe readiness, project-root detection, selected REPL path, and live session state.
• Added lean-probe capabilities CLI command with matching readiness output.
• Documented how LeanProbe complements LSP-backed Lean MCP tools such as lean-lsp-mcp.
• Updated tests for the new MCP and CLI capability surfaces.

Validation

• python -m pytest -q
• python -m ruff check .
• python -m build
• python -m twine check dist/*

LeanProbe 0.2.1

Patch release for LeanProbe MCP setup docs.

• Documents that stdio MCP clients should keep LEAN_PROBE_AUTO_BUILD=0.
• Explains that Lean/Lake projects should be built before starting LeanProbe MCP.
• Prevents MCP transport corruption from build output written to stdout.

Install:

python -m pip install -U lean-probe

MCP:

python -m pip install -U "lean-probe[mcp]"
lean-probe mcp

LeanProbe 0.2.0

First public LeanProbe release.

Install:

python -m pip install lean-probe

MCP support:

python -m pip install "lean-probe[mcp]"
lean-probe mcp

Highlights:

• Standalone Python package, CLI, and MCP server for LeanInteract-backed Lean feedback.
• Cached same-file declaration checks.
• Diagnostics, tactic metadata, proof-state stepping, and feedback_lean.
• Benchmarks for repeated target checks and sequential same-file checks.
• Python 3.10-3.13 support across Linux, macOS, and Windows.