Lean Beam

Lean Beam is an experimental project for efficient interaction with Lean from AI-assisted and tool-assisted workflows. It combines new Lean LSP extensions with a thin local broker. The extensions provide Lean-specific capabilities, and the broker exposes them through a lean-beam CLI and an MCP server for agent- and tool-facing workflows.

flowchart TB
  subgraph level1["Level 1: agents and tools"]
    cli["CLI / shell / agent"]
    mcp["MCP client / agent"]
  end

  subgraph level2["Level 2: Beam broker"]
    broker["Beam broker<br/>request routing<br/>session ownership"]
  end

  subgraph level3["Level 3: Lean instances"]
    subgraph lsp1["Lean LSP server"]
      lean1["Lean"]
      plugin1["Beam LSP plugin"]
    end
    subgraph lsp2["Lean LSP server"]
      lean2["Lean"]
      plugin2["Beam LSP plugin"]
    end
    subgraph lspn["Lean LSP server"]
      leanN["Lean"]
      pluginN["Beam LSP plugin"]
    end
  end

  cli -- lean-beam --> broker
  mcp -- lean-beam-mcp --> broker
  broker --> lsp1
  broker -- Lean LSP + Beam requests --> lsp2
  broker --> lspn
  lean1 --- plugin1
  lean2 --- plugin2
  leanN --- pluginN

Beam keeps the agent-facing surface small: clients talk to the broker, and the broker owns request routing plus one or more Lean LSP sessions with the Beam plugin loaded.

Beam lets a client try Lean commands or tactics at specific positions in saved files without changing those files. The central Beam extension is speculative execution through runAt, exposed by the CLI as lean-beam run-at and through MCP as lean_run_at. Because these probes can be issued concurrently, agents and tools can cheaply explore several "would this work here?" possibilities in the real module context.

Together, the LSP extensions, CLI, and MCP interface are intended to make that loop cheaper and more structured than repeatedly creating scratch files or using full lake build runs as the inner loop.

Beam is implemented in Lean, which lets it integrate more directly with Lean server state, saved snapshots, and synchronization where that matters.

We have found Beam useful for proof repair, proof search experiments, proof translation and porting, autoformalization experiments, and regular AI-assisted Lean editing.

Feedback is welcome through GitHub issues or Lean Zulip. For structured bug reports from a local checkout, lean-beam feedback --stdin can produce a pasteable report card; see docs/FEEDBACK.md.

Lean Beam is experimental beta software. It is not an official Lean FRO product. Current scope, limitations, and release direction are tracked in docs/STATUS.md.

Most readers should start with Install, then use docs/SETUP.md for toolchains, first CLI commands, agent-skill setup, and MCP registration. Release-facing changes are tracked in CHANGELOG.md.

Current Beta Surface

The current development line includes support for:

• speculative Lean execution with runAt
• incremental synchronization of Lean's view of a file after edits with sync
• actionable file information with todo, including sorries, holes, diagnostics, code actions, and incomplete proofs
• saving .olean artifacts from an interactive session with save
• selected Lean/LSP features through the same CLI and MCP interfaces, including hover, signature help, definitions, references, document/workspace symbols, and proof-state inspection
• feedback report cards for bug reports and project feedback through lean-beam feedback and MCP beam_feedback

See docs/STATUS.md for the current supported surface, known limitations, and release direction.

Install

Install or update Beam from a Lean Beam checkout:

./scripts/install-beam.sh

Run the installer again when you update the checkout and want the installed runtime to match it. Setup details, supported toolchains, agent-skill installation, MCP registration, direct CLI examples, installer locations, overrides, and offline advice live in docs/SETUP.md.

Lean Beam serves validated Lean toolchains listed in supported-lean-toolchains. See docs/SETUP.md for bundle setup and docs/CUSTOM_TOOLCHAINS.md for explicitly accepted local Lean builds.

Documentation Map

For users:

• docs/SETUP.md: install, toolchain, first-use, MCP, and installer reference.
• docs/CUSTOM_TOOLCHAINS.md: explicit local Lean toolchain support.
• docs/COMPATIBILITY.md: pre-stable compatibility policy and supported targets.
• docs/ROCQ.md: optional Rocq goal probes for Rocq-to-Lean porting.
• docs/FEEDBACK.md: feedback report cards for useful bug reports.
• docs/STATUS.md: current scope, limitations, and direction.
• CHANGELOG.md: release-facing changes.

For agent workflows:

• skills/lean-beam/SKILL.md: Lean workflow contract.
• skills/rocq-beam/SKILL.md: auxiliary Rocq workflow surface.

For contributors and maintainers:

• CONTRIBUTING.md: commit, PR, and contributor workflow guidance.
• docs/DEVELOPMENT.md: maintainer workflow and implementation notes.
• docs/TESTING.md: developer test-suite guidance and coverage map.
• docs/SYNC_AND_DIAGNOSTICS.md: sync, save, progress, diagnostics, and readiness contract.
• docs/MCP.md: current MCP maintainer architecture and conformance notes.
• AGENTS.md: repo-specific agent instructions.

Contributing And Help

The main goal of the beta development cycle is to gather feedback from Lean users and tool authors. Bug reports, design feedback, and documentation improvements are welcome through GitHub issues. Discussion is also welcome on the Lean Zulip.

Before contributing code or docs, read CONTRIBUTING.md. Maintainer workflow notes live in docs/DEVELOPMENT.md.

License

Apache-2.0. See LICENSE.