Lean Beam

Lean Beam gives AI agents and other tools an efficient way to work with Lean projects. It exposes Lean language-server extensions through a lean-beam CLI and an MCP server, keeping Lean's module context available across requests.

Beam supports:

• Speculative execution: try commands and tactics in a file's context without changing its source, using runAt. Independent attempts can run concurrently.
• Multi-file work: synchronize edited files and checkpoint modules so dependent files can use their changes.
• Saving from the running Lean context: save writes a module checkpoint from the state already checked by the Lean server, without batch re-elaboration.
• Diagnostics and pending work: sync waits for current diagnostics and readiness; todo finds sorries, holes, diagnostics, code actions, and incomplete proofs.
• Inspection and navigation: proof goals, hover and signature help, definitions, references, and document/workspace symbols.

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

Beam is implemented in Lean. CLI and MCP share broker code and typed operations, while each owns its transport and runtime lifetime:

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

  subgraph level2["Level 2: Beam runtime paths"]
    direction LR
    subgraph cliOwner["CLI lifetime"]
      direction TB
      cliAdapter["lean-beam<br/>foreground owner + private daemon"]
      cliRuntime["ServerRuntime<br/>single workspace"]
      cliAdapter --> cliRuntime
    end
    shared["shared typed operations<br/>admission + dispatch"]
    subgraph mcpOwner["MCP lifetime"]
      direction TB
      mcpAdapter["lean-beam-mcp<br/>multiplexed stdio"]
      mcpRuntime["ServerRuntime<br/>lazy multi-workspace"]
      mcpAdapter --> mcpRuntime
    end
  end

  subgraph level3["Level 3: Lean instances"]
    backends["one or more workspace backends<br/>Lean LSP + Beam plugin"]
  end

  cli --> cliAdapter
  mcp --> mcpAdapter
  cliRuntime -. uses .-> shared
  mcpRuntime -. uses .-> shared
  cliRuntime -- Beam requests --> backends
  mcpRuntime -- Beam requests --> backends

Loading

CLI clients use the project daemon owned by a foreground lean-beam serve process. An MCP client launches lean-beam-mcp, which manages its workspace sessions directly; it does not attach to the CLI daemon.

Beam is beta software, and its interfaces may change. See Status for current capabilities and limitations, and Compatibility for supported targets.

Install and connect your agent

Lean Beam is distributed in two ways:

• A Lean toolchain that includes Beam: follow bundled Beam setup. Use the commands provided by that toolchain for projects using the same Lean installation.
• A standalone installation: on Linux or macOS, run ./scripts/install-beam.sh from a Beam checkout with elan on PATH. The installer offers toolchains, agent skills, and MCP client registration.

Windows support is experimental. Native builds and CI do not establish an official elan Windows distribution path; that distribution is deferred pending the libuv investigation and fixes.

Bundled binaries do not install an agent skill. For either distribution, install the Lean agent skill from the matching Beam release, including its references directory, in your client's skill directory. To use MCP, also register the installed lean-beam-mcp command with your client; see MCP setup.

The standalone installer can do both. Run the command for your client:

./scripts/install-beam.sh --codex --codex-mcp
./scripts/install-beam.sh --claude --claude-mcp
./scripts/install-beam.sh --pi

The standalone installer puts commands in ~/.local/bin; make sure that directory is on PATH. Beam is installed once for your agent tools; you do not add it to each project's lakefile. For OpenCode, Mistral Vibe, manual MCP registration, additional toolchains, and offline setup, use the setup guide. Toolchains are selected when installing; runtime requests do not build missing Beam components.

Verify the connection

Restart your agent client after installation or a registration change so it loads the selected skills and server. From the Lean project, use lean-beam --version and lean-beam doctor to inspect the selected installation and project setup. For bundled commands, use the same elan run SELECTOR prefix described in bundled setup.

For MCP, use the client's connected tools to call beam_version, then lean_sync for an existing Lean file with its absolute workspace root. The first identifies the running server; the second checks the client-to-Lean request path. See MCP verification for details. A running server retains its original installation even after a launcher is updated; checking a newly launched command does not establish which version an existing client is using.

Before upgrading, stop existing sessions through their original installation and wait for cleanup. Follow the upgrade guide, then restart clients against the new installation.

Documentation

For users and agents:

• Setup: installation, agent skills, MCP registration, verification, and recovery.
• Agent workflow: commands, positions, versions, and outcomes.
• Trust and proof confirmation: checkpoints, batch builds, and independent proof confirmation.
• Status, Compatibility, and custom toolchains: capabilities, limitations, and supported targets.
• Changelog: release changes.

For contributors and integrators:

• Contributing and agent instructions: repository workflow.
• Development: architecture and maintainer guidance.
• Toolchain bundling: native runtime construction and distribution.
• MCP and Sync and diagnostics: protocol contracts.
• Testing: suites and coverage.

Beam is for non-adversarial development. Speculative requests isolate Lean elaboration state; they do not provide an OS sandbox for Lean IO. See sandbox permissions.

Rocq goal probes and the Rocq agent skill live in the separate, frozen rocq-beam project.

Help and feedback

Bug reports, design feedback, and documentation improvements are welcome through GitHub issues or Lean Zulip.

For a structured bug report, use lean-beam feedback-report --stdin as described in the feedback guide. Beam returns the report locally. Review it before sharing; for a non-public workspace, set "confidential": true in the input and share only privately.

License

Apache-2.0. See LICENSE.