Skip to content

LeanProbe 0.2.0

Choose a tag to compare

@Lemmy00 Lemmy00 released this 13 May 19:26
· 14 commits to main since this release

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.