Issues

• CLI sync loses response during import preparation while daemon remains live (custom Lean main)

  leanprover/lean-beam#411 · Filter by author ejgallego opened on Oct 29, 2026
  3

• Agent ergonomics follow-ups from the 0.2.0 RC review

  enhancement
  leanprover/lean-beam#407 · Filter by author ejgallego opened on Oct 28, 2026 · 0.3.0

• Keep newlines in readiness blocking diagnostics

  bug
  leanprover/lean-beam#406 · Filter by author ejgallego opened on Oct 28, 2026 · 0.3.0

• Do not report project style linters on runAt probe text

  bug
  leanprover/lean-beam#405 · Filter by author ejgallego opened on Oct 28, 2026 · 0.3.0

• Bound memory held by open documents

  enhancement
  leanprover/lean-beam#404 · Filter by author ejgallego opened on Oct 28, 2026 · 0.3.0

• runAt: blank lines and comments after a finished proof should select the command basis

  bug
  leanprover/lean-beam#403 · Filter by author ejgallego opened on Oct 28, 2026 · 0.3.0

• Detect stale transitive dependencies before reporting sync readiness

  bug
  leanprover/lean-beam#402 · Filter by author ejgallego opened on Oct 28, 2026 · 0.3.0

• runAt: a probe can use the declaration it is proving

  leanprover/lean-beam#389 · Filter by author ejgallego opened on Oct 27, 2026

• runAt: read multi-line text as if inserted at the probe position

  leanprover/lean-beam#388 · Filter by author ejgallego opened on Oct 27, 2026 · 0.3.0

• Qualify the actual 0.2.0 release artifacts

  leanprover/lean-beam#387 · Filter by author ejgallego opened on Oct 27, 2026 · 0.2.0
  6

• fix: make CLI recovery remedies usable from Windows shells

  leanprover/lean-beam#371 · Filter by author ejgallego opened on Oct 24, 2026

• Replace the temporary import basis capture with dependency watching and retained import artifacts

  leanprover/lean-beam#370 · Filter by author ejgallego opened on Oct 24, 2026

• Bound retention of recovered session descriptors

  enhancement
  leanprover/lean-beam#351 · Filter by author ejgallego opened on Oct 23, 2026 · 0.3.0

• Fail pending requests and recover after a Lean file worker dies

  bug
  leanprover/lean-beam#339 · Filter by author ejgallego opened on Oct 22, 2026 · 0.3.0

• Support supervised recovery after a session owner is killed

  enhancement
  leanprover/lean-beam#333 · Filter by author andtruth-agent opened on Oct 22, 2026 · 0.3.0

• Stop non-polling run-at probes after cancellation

  bug
  leanprover/lean-beam#331 · Filter by author ejgallego opened on Oct 21, 2026 · 0.3.0

• An external Lake build never clears a dependency's needsSave; the sync barrier then refuses the importer and the recovery plan points at save

  leanprover/lean-beam#256 · Filter by author spitters opened on Sep 12, 2026 · 0.3.0
  1

• Add a batch runAt API for source-position probe batches

  leanprover/lean-beam#101 · Filter by author ejgallego opened on Jun 22, 2026 · 0.3.0

• Support multi-command snippets in MCP lean_run_at

  leanprover/lean-beam#100 · Filter by author ejgallego opened on Jun 22, 2026 · 0.3.0