From e5454b7ec723edc71adc1cf08fda10e0935c2b06 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 7 Jul 2026 20:15:44 +0200 Subject: [PATCH 1/2] doc: compare Beam with related Lean tools --- CHANGELOG.md | 5 ++++ README.md | 6 ++++ docs/RELATED_TOOLS.md | 70 +++++++++++++++++++++++++++++++++++++++++++ docs/STATUS.md | 2 +- 4 files changed, 82 insertions(+), 1 deletion(-) create mode 100644 docs/RELATED_TOOLS.md diff --git a/CHANGELOG.md b/CHANGELOG.md index 7e866b78..6d746184 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,11 @@ This project keeps a lightweight, reverse-chronological changelog. Dates use `YY `--vibe-home`, and `VIBE_HOME` ([#213](https://github.com/ejgallego/lean-beam/pull/213), @archiebrowne). +### Documentation + +- Added a descriptive related-tools comparison for `lean-lsp-mcp`, Pantograph, and Beam's + saved-file probe layer. + ### Fixed - Module-mode `lean-save` and `lean-close-save` now checkpoint the complete Lake artifact family, diff --git a/README.md b/README.md index 9b2b235d..073cbe48 100644 --- a/README.md +++ b/README.md @@ -56,6 +56,10 @@ 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. +People comparing Lean tool integrations should also see +[docs/RELATED_TOOLS.md](docs/RELATED_TOOLS.md) for a descriptive comparison with `lean-lsp-mcp` and +Pantograph. + Beam is implemented in Lean, which lets it integrate more directly with Lean server state, saved snapshots, and synchronization where that matters. @@ -122,6 +126,8 @@ For users: targets. - [docs/ROCQ.md](docs/ROCQ.md): optional Rocq goal probes for Rocq-to-Lean porting. - [docs/FEEDBACK.md](docs/FEEDBACK.md): feedback report cards for useful bug reports. +- [docs/RELATED_TOOLS.md](docs/RELATED_TOOLS.md): descriptive comparison with nearby Lean agent and + proof-search tools. - [docs/STATUS.md](docs/STATUS.md): current scope, limitations, and direction. - [CHANGELOG.md](CHANGELOG.md): release-facing changes. diff --git a/docs/RELATED_TOOLS.md b/docs/RELATED_TOOLS.md new file mode 100644 index 00000000..c31385f8 --- /dev/null +++ b/docs/RELATED_TOOLS.md @@ -0,0 +1,70 @@ +# Related Tools + +This page explains where Lean Beam fits among nearby Lean tooling. It is descriptive, not a ranking +or replacement claim. The projects below expose different layers of Lean for different workflows, +and they may be useful together. + +The descriptions here are based on each project's public documentation and published material. For +complete and current details, read the linked project documentation directly. + +## Short Answer + +Lean Beam is centered on a small Lean-side extension plus a thin local broker. Its main operation is +an isolated, version-bound saved-file probe: `runAt(pos, "lean text")`. The broker exposes that same +operation model through the `lean-beam` CLI and `lean-beam-mcp`. + +[`lean-lsp-mcp`](https://github.com/oOo0oOo/lean-lsp-mcp) is an MCP server for Lean projects. Its +README describes agent interaction with Lean through LSP, including diagnostics, goal states, term +information, hover documentation, build-related tools, local source search, and external search +services. + +[`Pantograph`](https://github.com/stanford-centaur/PyPantograph) is a machine-to-machine interface +for Lean 4. The Pantograph paper presents it as an interface for advanced theorem proving, +high-level reasoning, and data extraction, with support for proof search workflows such as Monte +Carlo Tree Search. + +## Beam And lean-lsp-mcp + +Both Beam and `lean-lsp-mcp` support agent workflows around Lean projects, and both can expose an +MCP server. The main difference is the integration layer each project emphasizes. + +Beam starts from a Lean plugin and a small typed execution contract. The broker owns Lean LSP +sessions, routes requests, tracks document versions, and exposes CLI and MCP projections over the +same operation layer. This is why Beam emphasizes isolated saved-file probes, explicit `sync`, stale +version handling, saved snapshot checkpoints, and a deliberately small public request shape. + +`lean-lsp-mcp` exposes an MCP-facing Lean toolbox. Its documented surface includes Lean LSP +inspection tools, build-oriented tools, local project search, and external search services such as +Loogle and LeanSearch. + +Use Beam when the important loop is: try this Lean command or tactic here, in this saved module, +without changing the file, and keep the result tied to the document version. Use `lean-lsp-mcp` when +the important loop is: expose an MCP client to a Lean LSP, project-search, build, and theorem-search +toolbox. + +## Beam And Pantograph + +Beam and Pantograph are closer in spirit around machine-facing Lean interaction, but they are aimed +at different integration layers. + +Beam is an agent- and tool-facing local layer around Lean LSP plus Beam-specific extensions. Its +base workflow is intentionally narrow: update or sync a saved file, run an isolated probe at a +position, inspect messages and optional proof state, then make any accepted edit in the real source. +Beam is useful for proof repair, proof translation, autoformalization experiments, and AI-assisted +editing where the target remains an ordinary Lean project on disk. + +Pantograph is presented as a machine-to-machine interface for advanced theorem-proving systems. Its +paper emphasizes proof search, high-level reasoning, data extraction, and robust handling of Lean 4 +inference steps. Its public API is therefore a useful reference point for systems that need a +programmatic theorem-proving interface rather than a local CLI/MCP assistant surface. + +Use Beam when the client works against saved source files and needs isolated speculative checks in +the ordinary project context. Use Pantograph when the client is a theorem-proving system or research +harness that needs a programmatic proof-search, high-level reasoning, or Lean data-extraction +interface. + +## What Beam Is Not Trying To Replace + +Beam does not replace Lake, an editor, `lean-lsp-mcp`, Pantograph, theorem search, or prover +research frameworks. It occupies a specific layer: isolated speculative execution and related +saved-file operations, exposed consistently through a CLI, MCP server, and agent skill text. diff --git a/docs/STATUS.md b/docs/STATUS.md index fb3f2807..7bb6e2b7 100644 --- a/docs/STATUS.md +++ b/docs/STATUS.md @@ -223,7 +223,7 @@ Near-term work is mostly about hardening and simplifying: - keep the `sync`, `save`, and `close-save` summary projections aligned as the sync-summary schema evolves - keep Beam-daemon-side conveniences useful without turning them into a large public surface too early -- add a short comparison against Pantograph in the docs, to clarify where `runAt` fits among nearby Lean tooling +- keep the related-tools comparison current as nearby Lean agent and proof-search tooling evolves - keep cross-surface utility code such as root resolution and workspace-relative path derivation in shared Beam modules, not copied across CLI, broker, MCP, and test helpers From b3e6ee93c314b380a037f8a994051b3458349000 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 15 Jul 2026 19:32:19 +0200 Subject: [PATCH 2/2] doc: make related-tools comparison neutral --- docs/RELATED_TOOLS.md | 72 ++++++++++++++++++++++--------------------- 1 file changed, 37 insertions(+), 35 deletions(-) diff --git a/docs/RELATED_TOOLS.md b/docs/RELATED_TOOLS.md index c31385f8..f90e66b3 100644 --- a/docs/RELATED_TOOLS.md +++ b/docs/RELATED_TOOLS.md @@ -1,70 +1,72 @@ # Related Tools -This page explains where Lean Beam fits among nearby Lean tooling. It is descriptive, not a ranking -or replacement claim. The projects below expose different layers of Lean for different workflows, -and they may be useful together. +This page describes Lean Beam alongside two publicly documented Lean integrations: `lean-lsp-mcp` +and Pantograph. It is intended to help readers identify the interfaces relevant to their workflows; +it does not express a preference among the projects. Their scopes differ and may be complementary. The descriptions here are based on each project's public documentation and published material. For complete and current details, read the linked project documentation directly. ## Short Answer -Lean Beam is centered on a small Lean-side extension plus a thin local broker. Its main operation is -an isolated, version-bound saved-file probe: `runAt(pos, "lean text")`. The broker exposes that same -operation model through the `lean-beam` CLI and `lean-beam-mcp`. +Lean Beam consists of a Lean-side extension and a local broker. Its main operation is an isolated, +version-bound saved-file probe: `runAt(pos, "lean text")`. The broker exposes that operation model +through the `lean-beam` CLI and `lean-beam-mcp`. [`lean-lsp-mcp`](https://github.com/oOo0oOo/lean-lsp-mcp) is an MCP server for Lean projects. Its -README describes agent interaction with Lean through LSP, including diagnostics, goal states, term -information, hover documentation, build-related tools, local source search, and external search -services. +[README](https://github.com/oOo0oOo/lean-lsp-mcp#readme) and +[tools documentation](https://github.com/oOo0oOo/lean-lsp-mcp/blob/main/docs/tools.md) describe +agent interaction with Lean through LSP, including diagnostics, goal states, term information, +hover documentation, build-related tools, local source search, and external search services. [`Pantograph`](https://github.com/stanford-centaur/PyPantograph) is a machine-to-machine interface -for Lean 4. The Pantograph paper presents it as an interface for advanced theorem proving, -high-level reasoning, and data extraction, with support for proof search workflows such as Monte -Carlo Tree Search. +for Lean 4. The [Pantograph paper](https://arxiv.org/abs/2410.16429) presents it as an interface for +advanced theorem proving, high-level reasoning, and data extraction, with support for proof-search +workflows such as Monte Carlo Tree Search. ## Beam And lean-lsp-mcp Both Beam and `lean-lsp-mcp` support agent workflows around Lean projects, and both can expose an -MCP server. The main difference is the integration layer each project emphasizes. +MCP server. Their documentation emphasizes different integration layers. -Beam starts from a Lean plugin and a small typed execution contract. The broker owns Lean LSP +Beam starts from a Lean plugin and a typed execution contract. The broker owns Lean LSP sessions, routes requests, tracks document versions, and exposes CLI and MCP projections over the same operation layer. This is why Beam emphasizes isolated saved-file probes, explicit `sync`, stale -version handling, saved snapshot checkpoints, and a deliberately small public request shape. +version handling, saved snapshot checkpoints, and the public `runAt` request shape. `lean-lsp-mcp` exposes an MCP-facing Lean toolbox. Its documented surface includes Lean LSP inspection tools, build-oriented tools, local project search, and external search services such as Loogle and LeanSearch. -Use Beam when the important loop is: try this Lean command or tactic here, in this saved module, -without changing the file, and keep the result tied to the document version. Use `lean-lsp-mcp` when -the important loop is: expose an MCP client to a Lean LSP, project-search, build, and theorem-search -toolbox. +Beam's documented workflow centers on trying a Lean command or tactic at a position in a saved +module without changing the file, with the result tied to the document version. The documented +`lean-lsp-mcp` surface combines Lean LSP interaction with project search, builds, and theorem-search +services through MCP. ## Beam And Pantograph -Beam and Pantograph are closer in spirit around machine-facing Lean interaction, but they are aimed -at different integration layers. +Both projects expose machine-facing interaction with Lean. Their public documentation describes +different interfaces and client contexts. Beam is an agent- and tool-facing local layer around Lean LSP plus Beam-specific extensions. Its -base workflow is intentionally narrow: update or sync a saved file, run an isolated probe at a -position, inspect messages and optional proof state, then make any accepted edit in the real source. -Beam is useful for proof repair, proof translation, autoformalization experiments, and AI-assisted -editing where the target remains an ordinary Lean project on disk. +base workflow is to update or sync a saved file, run an isolated probe at a position, inspect +messages and optional proof state, then make any accepted edit in the real source. +Beam documents this workflow for proof repair, proof translation, autoformalization experiments, +and AI-assisted editing where the target remains an ordinary Lean project on disk. Pantograph is presented as a machine-to-machine interface for advanced theorem-proving systems. Its paper emphasizes proof search, high-level reasoning, data extraction, and robust handling of Lean 4 -inference steps. Its public API is therefore a useful reference point for systems that need a -programmatic theorem-proving interface rather than a local CLI/MCP assistant surface. +inference steps. Its README also documents programmatic tactic execution, metavariable coupling, +whole-file specification conformity checks, tactic-invocation data extraction, and inspection of +Lean constants. -Use Beam when the client works against saved source files and needs isolated speculative checks in -the ordinary project context. Use Pantograph when the client is a theorem-proving system or research -harness that needs a programmatic proof-search, high-level reasoning, or Lean data-extraction -interface. +Beam's request model is tied to saved project files and document versions. Pantograph documents a +programmatic interface for theorem-proving systems and research workflows involving proof search, +high-level reasoning, or Lean data extraction. -## What Beam Is Not Trying To Replace +## Scope Boundaries -Beam does not replace Lake, an editor, `lean-lsp-mcp`, Pantograph, theorem search, or prover -research frameworks. It occupies a specific layer: isolated speculative execution and related -saved-file operations, exposed consistently through a CLI, MCP server, and agent skill text. +Beam's documented scope is isolated speculative execution and related saved-file operations, +exposed through a CLI, MCP server, and agent skill text. Lake, editors, theorem-search services, +`lean-lsp-mcp`, Pantograph, and prover research frameworks provide other capabilities and +interfaces.