Skip to content

LAMP: Lean-based Agentic framework with MCP and Proof Repair

🕒 Published (v1): 2026-06-27 09:58 UTC · Source: Arxiv · link

Why this paper was selected

Novel MCP + formal verification (Lean) synthesis; proof repair for agent tool-use

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

LAMP is a multi-agent framework for generating kernel-verified Lean 4 proofs in domains absent from Mathlib. It combines a Planner (strategy), Builder (tactics), and Verifier (Lean kernel check) with MCP-based access to a curated domain ontology, achieving 96.7% on 90 Combinatorics on Words (CoW) theorems vs. 1.1–8.9% for specialized provers. The paper also contributes the first Lean 4 formalization of CoW (8 modules, 93 declarations).

Problem

LLMs produce unreliable proofs; interactive theorem provers like Lean 4 guarantee correctness via a small kernel, but their utility depends on formalized domain knowledge in Mathlib. Combinatorics on Words (CoW) — covering periodicity, borders, conjugacy, morphisms — has no Mathlib formalization, so both human formalizers and automated provers lack basic definitions and lemmas. State-of-the-art specialized provers (DeepSeek-Prover-V2, Goedel-Prover, Kimina-Prover) are trained on Mathlib-centered distributions and their performance collapses on unformalized domains, not because the reasoning is harder but because they lack vocabulary and supporting lemmas.

Method

Two artifacts:

  1. CoW Lean 4 library — 8 modules (Word, Factor, ProperPrefix, ProperSuffix, Border, Conjugacy, Period, Morphism) with a strict dependency hierarchy, containing 93 total declarations (22 definitions, 71 lemmas).

  2. LAMP multi-agent framework — coordinates three agents through a central Orchestrator:

  3. Planner: produces a mathematical proof strategy (no Lean code), names specific lemmas and techniques; retains persistent history to revise strategies after failure.
  4. Builder: translates the strategy into Lean tactics, querying the Semantic Toolbox via MCP (up to a fixed limit per attempt).
  5. Verifier: submits candidate proofs to a Lean 4 REPL and classifies results into errors/warnings/open goals/sorry occurrences; a proof is accepted only after passing both a textual sorry-check and a full REPL compilation.

The Semantic Toolbox exposes three MCP tool classes: a Lean LSP tool (ground-truth goal state), a Mathlib search tool (LeanExplore-based), and a curated CoW ontology (exact Lean statements, descriptions, source locations, dependencies, prerequisite chains). Tools follow a priority hierarchy: injected source → CoW ontology → Mathlib search.

Control flow is a dual-loop: an outer planning loop (up to \(R_{\max}\) re-plans) and an inner build loop (up to \(B_{\max}\) retries per strategy). Missing-definition errors trigger cheap re-grounding (context re-injection) without consuming a re-plan; genuine proof errors feed structured feedback to the Builder, with re-planning only after the inner budget is exhausted.

Key Contributions

  • First Lean 4 formalization of Combinatorics on Words (93 declarations across 8 modules)
  • LAMP: a multi-agent framework that injects domain knowledge at inference time via MCP-based CoW ontology, without retraining the backbone LLM
  • A CoW Evaluation Suite of 90 theorems across three difficulty levels, designed as a growing foundation (solved theorems fold back into the library)
  • Ablation isolating that both tool-grounded architecture and Planner/Builder separation are necessary for performance (each costs ~12 percentage points when removed)

Results

  • LAMP synthesizes verified proofs for 96.7% of 90 CoW theorems, spanning all eight modules and three difficulty levels
  • Unscaffolded LLM baseline: 58.9%
  • Existing specialized provers (DeepSeek-Prover-V2, Goedel-Prover, Kimina-Prover): 1.1–8.9% — "fail almost entirely because CoW lies outside their training distribution"
  • Ablation (backbone model held fixed):
  • Removing LAMP's tool-grounded architecture: ~12 percentage point drop
  • Removing Planner/Builder separation: ~12 percentage point drop
  • Out-of-domain benchmarks: LAMP is "deliberately less competitive" — trades breadth for depth

Limitations

  • Performance depends on the curated CoW ontology; building such ontologies for new domains is labor-intensive
  • LAMP trades breadth across general mathematics for depth in an unformalized domain (deliberately uncompetitive on out-of-domain benchmarks)
  • The CoW library is small (93 declarations) — foundational but not yet comprehensive
  • Requires a frontier LLM API (cost and latency of multi-agent rounds with tool calls)
  • Bounded attempt budget (\(R_{\max} \times B_{\max}\)) means some proofs exhaust attempts and fail

Relevance to Harnesses / Meta-Harnesses

LAMP is a direct example of a meta-harness for theorem proving: it decomposes a complex cognitive task (proof synthesis) into specialized agents (Planner, Builder, Verifier) coordinated by a central Orchestrator with a dual-loop control flow. Its explicit grounding in MCP-based tools rather than model weights — the Semantic Toolbox providing a CoW ontology, Lean LSP for ground-truth goal states, and a priority-ordered tool hierarchy — exemplifies the harness pattern of augmenting LLMs with structured external knowledge to overcome training-distribution limitations. The finding that both tool-grounding and agent separation contribute ~12 points each isolates the value of architectural decomposition beyond the backbone model, directly relevant to the design of future meta-harness systems.