# Lean Beam

> Use this when an AI should work on an external Lean project through the installed `lean-beam` wrapper, giving it direct efficient access to Lean's proof engine to avoid rebuilds through cheap speculative checks and zero-build module checkpoints.

- **Type:** Skill
- **Install:** `agentstack add skill-ejgallego-lean-beam-lean-beam`
- **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior
- **Seller:** [ejgallego](https://agentstack.voostack.com/s/ejgallego)
- **Installs:** 0
- **Category:** [Agent Skills](https://agentstack.voostack.com/c/agent-skills)
- **Latest version:** 0.1.0
- **License:** Apache-2.0
- **Upstream author:** [ejgallego](https://github.com/ejgallego)
- **Source:** https://github.com/ejgallego/lean-beam/tree/main/skills/lean-beam

## Install

```sh
agentstack add skill-ejgallego-lean-beam-lean-beam
```

Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent.

## About

# Lean Beam

Use this skill for Lean projects when you want the AI to replace repeated `lake build` loops with cheap speculative Lean probes, optional follow-up handle execution, and targeted file checkpoints.

This is the Lean-only skill. It should stay focused on Lean and should not require Rocq setup or Rocq concepts.
Do not factor shared Lean/Rocq skill instructions into a common helper; duplicate short guidance if
both skills need it.

## Setup

From the `lean-beam` repo root:

```bash
./scripts/install-beam.sh --codex
```

Use `--claude`, `--pi`, `--opencode`, or `--vibe` instead when installing for Claude Code,
Pi Agent, OpenCode, or Mistral Vibe. Use `--all-skills` when you want every supported agent skill
target.

The installer puts `lean-beam`, `lean-beam-search`, and `lean-beam-mcp` in `~/.local/bin`, stages
the self-contained runtime under `BEAM_INSTALL_ROOT` (default `~/.local/share/beam`), requires
`elan` on `PATH`, prebuilds the pinned `lean-toolchain` bundle by default, and installs the bundled
Lean skill only for the agent flags you request. Use the setup docs for additional supported or
custom toolchain prebuilds.

Use `lean-beam --version` for CLI bug reports and installed runtime identity checks. Use
`lean-beam-mcp --version` to verify which installed MCP server wrapper, server binary, runtime
payload hash, manifest, and source commit a client command resolves. Source checkout runs also
report git commit/branch/dirty state when available. From a live MCP session, call `beam_version`
to report the running server process identity as structured content.
`lean_init_workspace` with `mode: "reset"` restarts the Lean runtime inside the current MCP server
process; it does not prove the MCP server binary itself was refreshed.

Restart active agent or MCP client sessions after installation.

For the authoritative install and bundle-resolution order, see the repo
[docs/SETUP.md](../../docs/SETUP.md) and [Supported Toolchains](../../docs/SETUP.md#supported-toolchains-and-bundles)
sections.

## Skill Surface

This skill documents the current Lean-facing `lean-beam` workflow surface. Use the smallest command
family that fits the task.

Agents may access Beam through the `lean-beam` wrapper or through a registered `lean-beam-mcp`
server. This skill names wrapper commands because they are always available after installation. When
your client exposes the matching MCP tools, use them with the same saved-file, version, update, sync,
and isolation rules; do not treat MCP as a raw Lean LSP proxy.

Supported command families:

- bootstrap the Lean backend: `lean-beam ensure`
- keep a sandboxed daemon owner alive across separate commands: `lean-beam ensure --hold`
- inspect existing code, navigation data, or proof state: `lean-beam hover`,
  `lean-beam signature-help`, `lean-beam definition`, `lean-beam references`,
  `lean-beam document-symbols`, `lean-beam workspace-symbols`, `lean-beam goals before`,
  `lean-beam goals after`
- inspect actionable Lean items in a range: `lean-beam todo`
- inspect file or daemon state: `lean-beam open-files`, `lean-beam doctor`, `lean-beam stats`,
  `lean-beam reset-stats`
- produce a pasteable bug report card from JSON input: `lean-beam feedback`
- try one isolated speculative Lean snippet: `lean-beam run-at`
- continue from one exact speculative state: `lean-beam run-at-handle`, `lean-beam run-with`,
  `lean-beam run-with-linear`, `lean-beam release`
- refresh or checkpoint one tracked workspace module: `lean-beam sync`, `lean-beam refresh`,
  `lean-beam save`, `lean-beam close-save`
- run shell-oriented search loops over the same handle APIs: `lean-beam-search`

What to treat as the normal agent workflow surface:

- default workflow commands: `lean-beam hover`, `lean-beam signature-help`,
  `lean-beam definition`, `lean-beam references`, `lean-beam document-symbols`,
  `lean-beam workspace-symbols`, `lean-beam goals`, `lean-beam todo`, `lean-beam run-at`,
  `lean-beam sync`,
  `lean-beam refresh`
- operational commands: `lean-beam open-files`, `lean-beam doctor`,
  `lean-beam stats`, `lean-beam reset-stats`, `lean-beam feedback`, `lean-beam save`,
  `lean-beam close-save`
- pre-stable support APIs: `lean-beam run-at-handle`, `lean-beam run-with`, `lean-beam run-with-linear`,
  `lean-beam release`, `lean-beam-search`

Core workflow contract:

- use `lean-beam`, not raw JSON and not raw LSP
- `lean-beam` only sees the on-disk file, not unsaved editor buffers
- in transient PID-sandboxed command runners, start one foreground `lean-beam ensure --hold`
  process when you need daemon reuse across separate shell invocations; interrupt it when finished
- after every real Lean source edit: save the file normally, then run `lean-beam update` before the
  next version-bound probe; run `lean-beam sync` when you need diagnostics/readiness
- use `lean-beam save` only for a synced workspace module path in the current Lake workspace package
  graph, for example `MyPkg/Sub/Module.lean`
- `lean-beam save` validates and checkpoints only the module you save; it does not validate importers of
  that module
- `lean-beam save` currently supports only Lake module setups Beam can replay from the LSP snapshot
  without custom batch setup; modules with custom Lean options, Lean arguments, dynamic libraries, or
  plugins fail with `saveUnsupportedSetup` and should be rebuilt with `lake build`
- treat wrapper `stderr` as human-facing only; use stdout JSON or `beam-client request-stream`
  for machine-readable automation
- `lean-beam feedback` does not accept free-form notes; pass a JSON object with required string
  fields `title`, `summary`, `reproduction`, `expected`, and `actual`
- use optional feedback triage fields `kind` (`bug`, `ux`, `perf`, `docs`, `question`) and
  `severity` (`low`, `medium`, `high`, `critical`) when they help route the report
- do not assume hidden mutable session state carries across unrelated requests

## Agent Cost Model

Prefer Beam probes over detached scratch Lean files for project-local questions.

A standalone scratch file has a high fixed cost: it starts from a detached module, reloads imports
and environment, and encourages simplified contexts that may not match the real source position.

A `lean-beam run-at` probe has low marginal cost once the per-project daemon and module context are
warm: it asks one speculative question against an explicit broker document version and the real
module environment.

This changes the right agent behavior:

- prefer many small `run-at` probes at the source position over one large scratch experiment
- use `goals before`, `goals after`, `hover`, `signature-help`, `definition`, `references`, and
  symbol queries instead of reconstructing semantic state elsewhere
- issue independent `run-at` probes or handle-rooted search sequences in parallel when you have many
  candidates to check; use distinct request IDs if you need per-request cancellation or tracing
- do not batch unrelated questions just to amortize Lean startup; future batch APIs may reduce
  per-call overhead, but high-bandwidth clients can already get most of the throughput benefit by
  keeping independent probe sequences in flight
- after a real source edit, run `lean-beam update ` before later probes; run
  `lean-beam sync ` when you need diagnostics/readiness
- use `lake build` for dependency-cone or final validation, not as the inner loop
- use scratch files only for context-free Lean syntax checks or Beam incident isolation

## Prompting Contract

Prefer the smallest command that matches the actual task:

- use `lean-beam hover` when you want semantic information about existing code at one position
- use `lean-beam signature-help` when you want callable-argument signature information at one
  position
- use `lean-beam definition` or `lean-beam references` when you want navigation targets for an
  existing symbol
- use `lean-beam document-symbols` for file-local symbol outlines and `lean-beam workspace-symbols`
  for workspace-wide symbol search
- use `lean-beam goals before` or `lean-beam goals after` when you want existing proof state at one
  tactic position
- use `lean-beam todo` when you want actionable items in a saved file range, such as sorries, holes,
  diagnostics, code actions, or incomplete proofs
- use `lean-beam run-at` when you want to try one speculative Lean snippet without editing the file
- before `lean-beam run-at`, `lean-beam run-at-handle`, `lean-beam hover`,
  `lean-beam signature-help`, `lean-beam definition`, `lean-beam references`,
  `lean-beam document-symbols`, `lean-beam goals`, or `lean-beam todo`, call
  `lean-beam update ` and pass the returned `version`; `lean-beam workspace-symbols` takes
  only a query
- if a versioned request fails with `contentModified` and
  `error.data.reason = "documentVersionMismatch"`, use `error.data.acceptedVersion` for the next
  retry or run `lean-beam update` / `lean-beam sync` again; do not guess a version
- for `lean-beam run-at`, `lean-beam hover`, `lean-beam signature-help`,
  `lean-beam definition`, `lean-beam references`, `lean-beam goals`, and `lean-beam todo`, treat
  line and character arguments as Lean/LSP coordinates: line `0` is the first line, character `0`
  is the first UTF-16 code unit, and on a truly empty line only character `0` is valid
- use `lean-beam run-at-handle` and then `lean-beam run-with` or `lean-beam run-with-linear` only when exact
  speculative continuation matters
- for multiline speculative text, prefer `--stdin` as the normal path; use `--text-file `
  when the text already lives in a file
- for handle-based continuation, prefer `--handle-file ` as the normal path; deeper shell-loop
  variants such as stdin handle piping live in the reference docs
- do not expect one `lean-beam run-at` call to become the basis of the next one automatically
- parallel probes are fine when they are independent; do not concurrently reuse a linear handle or
  assume ordered side effects between separate speculative sequences
- use `lean-beam update` right after every real saved edit before the next speculative probe
- use `lean-beam sync` when you need diagnostics/readiness before saving or checkpointing
- use `lean-beam save` or `lean-beam close-save` only for a synced workspace module path such as
  `MyPkg/Sub/Module.lean`

Stop probing and change tactics when:

- the speculative result now needs to become real source: edit the file, save it, then `lean-beam sync`
- repeated `lean-beam run-at` probes are no longer clarifying the problem
- you edited a dependency and now need trustworthy downstream results; `lean-beam save` only validates
  the module you save, not downstream importers
- stale-state, `contentModified`, or rebuild trouble keeps appearing; inspect with `lean-beam open-files`
  and `lean-beam doctor`
- if `lean-beam sync` fails with `syncBarrierIncomplete`: inspect `error.data.staleDirectDeps`,
  `error.data.saveDeps`, and `error.data.recoveryPlan`; save only the listed direct deps that still
  need checkpointing, then `lean-beam refresh "Target.lean"` if the plan says to;
  if this repeats across multiple dependency hops, escalate to `lake build`

When those conditions hold, prefer a real edit plus `lean-beam sync`, or escalate to `lake build` when
the task has become dependency freshness or final validation across importers rather than one-file
probing.

## Lean-Run-At Semantics

`lean-beam run-at` is a speculative execution request against one explicit broker document version.
Read it as "try this Lean text here", not as "edit the file here".

What `lean-beam run-at` does not do:

- it does not edit the source file or create a new on-disk baseline for the next request
- it does not make the speculative text become the basis of the next `lean-beam run-at` call
- it does not wait for or return the full diagnostics barrier for the rest of the file
- it does not replay full-file diagnostics in its final JSON payload
- it does not auto-indent or synthesize leading spaces when you probe at an indented empty line
- it does not reinterpret blank-line coordinates; if the line is truly empty then character `1` is
  already out of range
- in command mode, one `run-at` request accepts one Lean command, not a complete top-level command
  sequence; use `run-at-handle` plus `run-with` for explicit sequencing, or make a real edit and
  `sync`

Use the right tool for each goal:

- if you made a real edit and want fresh file diagnostics: save the file, then use `lean-beam sync`
- if you want exact continuation from speculative state: mint a handle with `lean-beam run-at-handle`,
  then continue with `lean-beam run-with` or `lean-beam run-with-linear`
- if you want to test several top-level commands together: write them to the file and sync, or split
  the experiment into explicit handle continuations
- for handle-based commands, `--handle-file ` is the easiest way to avoid inlining handle json
- if surface syntax depends on indentation or layout: pass the exact text you want Lean to parse, or
  make a real edit in the file instead of expecting the wrapper to fill whitespace for you

Open [references/lean-run-at-semantics.md](references/lean-run-at-semantics.md) when the task needs
concrete examples for:

- full-file diagnostics after a speculative probe
- chaining speculative state across multiple calls
- indentation-sensitive or newline-sensitive probes on blank or layout-sensitive lines

Open [references/workflow-details.md](references/workflow-details.md) when the task needs the shell-oriented
details for:

- `--text-file`, `--`, or stdin-handle piping variants
- handle-file versus stdin-handle tradeoffs
- debugging-oriented wrapper details instead of the normal path

Open [references/commit-speculative.md](references/commit-speculative.md) when the task needs the
current workflow for turning a good speculative probe into a real saved edit.

Open [references/anti-patterns.md](references/anti-patterns.md) when you want a short checklist of
what Lean agents should not assume about `lean-beam run-at`, `lean-beam sync`, handles, or dependency edits.

## Lean Wrapper

Use `lean-beam`, not raw JSON and not raw LSP.

`lean-beam` for Lean:

- infers the target project root from the current directory or `--root`
- keeps one Beam daemon per project root and records it in `/.beam/beam-daemon.json`
  - in sandboxed or read-only project trees, set `BEAM_CONTROL_DIR` to a writable directory; `lean-beam` uses a per-root subdirectory there
- resolves a toolchain-keyed Lean bundle, preferring the installed beam bundle cache and
  falling back to a project-local runtime bundle under `/.beam/bundles` or `BEAM_BUNDLE_DIR`
- serves Lean toolchains listed in `supported-lean-toolchains` plus exact custom names recorded by
  the installer in `custom-lean-toolchains`
- owns Beam daemon startup, shutdown, and registry handling
- resolves Lean with `elan which lean`
- builds a local fallback bundle only when no matching installed bundle exists for the target
  supported or explicitly custom Lean toolchain
- fails early on Lean toolchains that are neither supported nor explicitly custom; use
  `lean-beam supported-toolchains` to inspect the validated allowlist and `lean-beam doctor` to
  inspect custom acceptance state
- restarts the Beam daemon if the effective Lean startup configuration for that root changes
- `lean-beam shutdown`, `lean-beam stats`, and `lean-beam reset-stats` apply to the current project only
- wrapper commands talk to the per-project Beam daemon over localhost TCP; they are not direct in-process Lean calls
- `lean-beam ensure --hold` prints the usual JSON ensure response on stdout, keeps the wrapper
  process alive until interrupted, and is only for environments that reap background daemons when
  each command exits; later wrappers recover from same-namespace stale lease files left by killed
  wrapper processes

`lean-beam` is more than a one-shot probe:

- the common path is stil

…

## Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

- **Author:** [ejgallego](https://github.com/ejgallego)
- **Source:** [ejgallego/lean-beam](https://github.com/ejgallego/lean-beam)
- **License:** Apache-2.0

Install and usage instructions live in the source repository linked above.

## Pricing

- **Free** — Free

## Security capabilities

Automated source analysis of v0.1.0 — what this tool can access:

- **Network access:** no
- **Filesystem access:** no
- **Shell / process execution:** no
- **Environment & secrets:** no
- **Dynamic code execution:** no

*"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.*


## Versions

- **0.1.0** — security scan: passed — Imported from the upstream source.

## Links

- Listing page: https://agentstack.voostack.com/l/skill-ejgallego-lean-beam-lean-beam
- Seller: https://agentstack.voostack.com/s/ejgallego
- Browse the marketplace: https://agentstack.voostack.com/browse

---
Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.