leanprover/lean-beam

Claude/Codex skill and local workflow layer for efficient interaction with Lean 4 and Monte-Carlo Tree Search.

Stars: 31
Forks: 4
Open beginner issues: 1
Indexed issues: 5
Avg merge: 1d 13h
Merged PRs (30d): 12

Dominant language: Lean
License: Apache-2.0
Last GitHub push: Sep 7, 2026
Latest indexed: Sep 20, 2026
Contributing guide: Contributing guide
Code of conduct: No code of conduct
Beginner labels: No beginner labels indexed

Beginner friendly Everything

Open All

Docs: lean_sync runs setup-file and builds stale imports; the daemon pins the toolchain under .beam Open

Difficulty 2/5 1-3 hours Newbie friendliness 70/100

leanprover/lean-beam#257 · Opened Sep 12, 2026
An external Lake build never clears a dependency's needsSave; the sync barrier then refuses the importer and the recovery plan points at save Open

Difficulty 4/5 3-5 days Newbie friendliness 52/100

leanprover/lean-beam#256 · Opened Sep 12, 2026
lean_save hangs to the client idle timeout instead of returning saveUnsupportedSetup in a package with batch-only moreLeanArgs Open

Difficulty 4/5 3-5 days Newbie friendliness 52/100

leanprover/lean-beam#255 · Opened Sep 12, 2026
Add a batch runAt API for source-position probe batches Open

Difficulty 5/5 Over a week Newbie friendliness 45/100

leanprover/lean-beam#101 · Opened Jun 22, 2026
Support multi-command snippets in MCP lean_run_at Open

Difficulty 4/5 3-5 days Newbie friendliness 48/100

leanprover/lean-beam#100 · Opened Jun 22, 2026

A short digest of beginner-friendly GitHub issues.