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

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked every number, table and page reference, algorithm line, quotation, technique steps and ablation figures against the text and Tables 1-10; corrected eleven versus twelve have-statements in the Appendix C proof, the 38 failures described as theorems, the 62 point spread (62.5), the unsupported claim about the provers’ own sampling, the unmarked trusted-base inference, the ontology-record step the paper does not give, and the Section 4.4 evidence for the 58.9% baseline; Verus forms not run through Verus and left unchanged.

source: Santhana Srinivasan R and Maithilee Patawar, arXiv:2606.28841v1 (27 Jun 2026), 25 pages with appendices A–C. Page numbers below are the PDF’s running page numbers.

what the paper proves or measures

Two artifacts. First, a Lean 4 library for combinatorics on words (CoW: prefixes, suffixes, borders, periods, conjugacy, morphisms of finite sequences), 22 definitions and 71 lemmas, 93 declarations in 8 modules (Table 1, p.7). Second, LAMP, an agent loop of a Planner, a Builder and a Verifier around one general-purpose LLM, which fills a sorry in a theorem over that library. The measured headline: “LAMP solves 87 of 90 theorems, an overall pass rate of 96.7%.” (Section 4.2, p.13). 87/90 = 96.7%, checked.

The claim the paper wants the reader to take away is about where proving ability in a new domain comes from: “Our main observation is that an unformalized domain needs explicit and structured domain knowledge at inference time, rather than knowledge that is only learned implicitly through training.” (Section 1, p.2)

What stays trusted: the Lean kernel and the 90 theorem statements, which the authors wrote themselves (the suite is self-constructed, Section 5, p.17). One of the 90 statements is false (see the part on contradictions). Inference: this suggests the statements were not independently checked.

Inference: nothing in the paper is about programs. All 90 targets are lemmas about lists. What transfers to Verus is the scaffolding around a proof search, and the way the library was shaped so that proofs avoid index arithmetic.

technique 1: inject the verbatim source of the imported modules

what it is: before any LLM call, the controller reads the target file’s imports, finds the library files they name, and pastes those files whole into both agents’ prompts.

when to use: the proof must use definitions and lemma names that the model has never seen in training, and the library is small enough to paste.

how it is done (Section 3.3, Orchestrator, p.9; Algorithm 1 line 1, p.11):

1. extract the import statements of the target theorem’s file
2. resolve each import to its library source file
3. put the source text, unchanged, in the Planner prompt and in the Builder prompt (C ← LoadContext(T, L))

The paper’s reason: “This ensures the agents reason about the library’s actual definitions and lemma names rather than plausible-looking inventions, which is the principal defense against hallucinated identifiers.” (Section 3.3, p.9)

Verus form (Inference: the paper has no Verus): resolve the use lines of the Rust file under proof, and paste the full text of each imported module’s spec fn and proof fn signatures with their requires and ensures. For a closed spec fn only the signature helps the caller, because its body is hidden outside its module. Lemmas of vstd that the file uses belong in the same paste. What does not carry over: the size bound. The CoW library has 93 declarations; a Verus project with thousands of lemmas cannot be pasted whole, and the paper does not test that case.

evidence: no ablation removes this step. Both ablations keep it: “We test this with two ablations, holding the 3 × 3 attempt budget and injected library source fixed in both.” (Section 4.3, p.13). The baseline row “Backbone LLM, no agents” at 58.9% (53/90; Table 6, p.14) is described only as given “the same ontology context”, so the paper has no number for a model without the library text. Its effect is therefore asserted, not measured.

limits: Inference: it scales with library size, and it only prevents invented names for the pasted modules.

technique 2: a domain ontology served as a tool, consulted in a fixed order

what it is: a curated record per library entity that a tool returns on request, plus two graph queries. The paper’s description of the record: the tool answers “returning the exact Lean statement, description, source location, dependencies, and related concepts for a named CoW entity, together with operations that list all lemmas in a conceptual family or return a theorem’s prerequisite chain” (Section 3.3, Semantic Toolbox, p.10; the quoted words are the end of a longer sentence).

when to use: the Builder needs one fact (the exact statement of a lemma, or which lemmas exist about borders) and should not rely on recall.

how it is done (Section 3.3, p.9–10):

1. (not in the paper; the paper says only that the corpus is curated and does not say how it was built) write, for every definition and lemma, the fields listed above: statement, description, source location, dependencies, related concepts
2. expose three operations through MCP: lookup by name, list a concept family, return a prerequisite chain
3. add two generic tools beside it: a Lean language-server tool that returns the goal state at a sorry, and a Mathlib search tool built on LeanExplore
4. state the order of consultation in the prompt: “the Builder consults the injected source first, then the CoW ontology for domain-specific lookups, and only as a last resort the broader Mathlib search” (p.10)
5. cap the number of tool queries per build attempt; the paper says “up to a fixed limit per attempt” (Builder Agent, p.9) and does not give the limit

The paper does not show the ontology’s file format, an example record, or how the records were produced. Section 2.3 (p.6) says the ontology is “also consumed by a dedicated Planner agent during proof-strategy formation”, but Algorithm 1 (p.11) passes Toolbox only to Builder; how the Planner reads it is not specified.

Verus form (Inference): one record per spec fn and proof fn: its signature with requires/ensures, the file and line, the spec fns its contract mentions (dependencies), and sibling lemmas (family). The prerequisite chain is the set of proof fns a lemma’s body calls, transitively. The Mathlib search maps to a search over vstd lemma names and broadcast groups. The goal-state tool does not carry over: Verus has no tactic goal state. The nearest ground truth is the verifier’s report of which assert, ensures or invariant failed.

evidence: the “no MCP” ablation, same backbone (Kimi K2.6) and the same 9-call budget (Table 4, p.14): overall 84.4% against 96.7% for the full system; Hard theorems 47.1% against 88.2%; Medium 91.4% against 98.3%; Easy 100.0% in both. In counts these are 76/90 against 87/90, 8/17 against 15/17, 53/58 against 57/58 (Inference: counts computed from the percentages and Table 2’s sizes; they sum to 76).

limits: “No MCP removes all tool access.” (Section 4.3, p.13) So the 12.3-point loss is the joint effect of the ontology, the goal-state tool and the Mathlib search; the ontology alone is not isolated. Inference: since the library source is already in the prompt, the ontology mostly re-serves text the model has; the goal-state tool may account for much of the Hard-theorem gain. The paper’s discussion credits “curated domain tooling” without separating the three.

technique 3: split strategy from tactics, with two nested retry loops

what it is: one agent writes a plan in prose naming lemmas, another writes the proof text; a failed proof is first retried by the second agent, and only after its budget is spent does the first agent re-plan.

when to use: failures are of two kinds that cost differently to fix, a wrong mathematical approach and a right approach written wrongly. The paper: “Separating strategy from implementation in this way lets the system distinguish a flawed mathematical approach (which warrants re-planning) from a correct approach that was implemented incorrectly (which warrants only a rebuild).” (Planner Agent, p.9)

how it is done (Algorithm 1, p.11; Section 3.4, p.10–11):

1. HP ← ∅: start an empty Planner history that lasts the whole run (line 2)
2. outer loop, r from 1 to Rmax: plan ← Planner(T, C, HP); the plan is “an explicit chain-of-thought analysis followed by a structured plan that names the specific library lemmas and the proof technique to apply” (p.9; part of a longer sentence) and contains no Lean code (line 4)
3. HB ← ∅: reset the Builder history for this plan (line 5)
4. inner loop, b from 1 to Bmax: proof ← Builder(plan, C, HB, Toolbox) (line 7)
5. check the proof (technique 4); on success return it (lines 8–14)
6. on failure add the structured errors to HB, so that “the next attempt receives the structured error and the prior code” (Builder Agent, p.9) (lines 17 and 19)
7. when the inner loop ends without success, add a summary of the failed attempts for this plan to HP and re-plan (line 22)
8. after Rmax plans return failure (line 24)

Budget used in every experiment: “Rmax = 3 re-plans and Bmax = 3 build attempts per plan” (Section 4.1, p.12), so at most 9 verifications per theorem, each with a 30-second timeout (p.13).

Verus form (Inference): the plan names which proof fn lemmas to call, which induction variable carries the decreases, and which intermediate asserts to state; the Builder writes the proof fn body or the proof { } block and the loop invariants. The split carries over unchanged. What changes: in Verus a plan may also need to change executable code or a loop invariant, which is not a proof body; the paper’s Builder edits only a proof body.

evidence: “single agent” ablation, same backbone, Planner removed and the Builder given all 9 calls with full tool access (Table 4, p.14): overall 85.6% against 96.7%; Hard 58.8% against 88.2%; Medium 89.7% against 98.3%; Easy 100.0% in both. The paper’s summary: “Both ablations cost a comparable 11–12 points overall, with the loss concentrated almost entirely in Hard theorems (88.2% down to 47.1% and 58.8%); Easy theorems are unaffected.” (Section 4.3, p.13)

limits: each configuration was run once per theorem (pass@1) at temperature 1, the only value the Kimi K2.6 API accepts (p.13), with no repeated runs or variance. Inference: on 17 Hard theorems one theorem is 5.9 points, so the difference between the two ablations (8/17 and 10/17) is two theorems and not evidence that one component matters more.

technique 4: accept a proof only after a text check and a completeness check

what it is: two gates. A string search for the placeholder, then a compile whose result must have no errors, no placeholders and no placeholder warnings.

when to use: always, when the proof language has an escape hatch that type-checks.

how it is done (Section 3.4, Dual-stage verification, p.10; Algorithm 1 lines 8–14; Verifier, p.10):

1. if the proof text contains the token sorry, do not compile; record “proof still contains sorry” in the Builder history and try again
2. otherwise submit it to a Lean 4 REPL
3. parse the REPL output into four classes: errors, warnings, open goals, sorry occurrences
4. call the result “pass” when there are no errors and “complete” when there are also no sorries and no sorry-warnings; accept only “complete”
5. return parsed errors with the offending goal state to the agents

Why both: “The textual stage is necessary because Lean accepts sorry as a well-typed placeholder: a proof consisting of sorry alone compiles without error, so a compilation pass alone would register a false success.” (Section 3.4, p.10)

The Verifier runs many checks at once: the backend “runs REPL instances as isolated worker processes with per-process resource limits and timeouts, and a scheduler reaps stale processes” (p.10; part of a longer sentence).

Verus form (Inference): the escape hatches to search for are admit(), assume(...), assume(false), #[verifier::external_body] and assume_specification added by the agent. A textual search before running Verus is the same step. The second gate is: Verus reports zero errors for the whole crate, and the contract of the target function (requires, ensures) is byte-identical to the one given. The paper’s step 4 distinction also applies: a file that verifies with an admit() inside is “pass”, not “complete”.

evidence: none separate; the paper reports no count of proofs caught by either gate.

limits: Inference: the text check is for one token. It does not catch a theorem statement that was weakened; the paper relies on technique 6 for that. It also does not catch a proof that closes the goal with an added axiom; the paper does not mention axioms.

technique 5: treat “name not found” as a cheap failure

what it is: a branch in the inner loop. If the compile error says a definition or lemma does not exist, reload the library context and let the Builder try again under the same plan.

when to use: the error is about addressing, not reasoning. The paper: “If the error indicates that a referenced definition or lemma could … not be found, this represents an addressing failure rather than a flaw in the strategy.” (Section 3.4; the sentence runs from p.10 to p.11, and the ellipsis stands only for the page break)

how it is done (Algorithm 1 lines 15–17, p.11):

1. classify the result with IsMissingDefinition(res)
2. if true, C ← ReloadContext(T, L) and append the errors to HB
3. continue the inner loop with the same plan

The paper’s summary of the design: “This separation keeps inexpensive recovery (re-grounding) distinct from expensive recovery (re-planning).” (Section 3.4, p.11)

Verus form (Inference): the matching errors are the Rust compiler’s unresolved-name errors for a proof fn or spec fn that does not exist. Re-show the signatures of the module the name was expected in, and keep the plan.

evidence: none separate.

limits: in the listing this branch still uses up one of the Bmax inner iterations, so it is not free. Inference: after three invented names in a row the plan is dropped although nothing was wrong with it.

technique 6: patch only the proof body

what it is: the controller, not the model, decides which characters of the file may change.

how it is done (Orchestrator, p.9; Builder Agent, p.9; Appendix C, p.24–25):

1. a theorem locator finds the source region of the target proof
2. generated tactics replace only the sorry body
3. if the region’s boundaries cannot be found, replace only the lines that contain sorry
4. strip from the Builder’s output any repeated theorem signature before patching

The paper states the guarantee: “The Orchestrator’s edit localization (Section 3.3) means only the proof body changes between input and output; the theorem signature is never touched.” (Appendix C, p.24)

Verus form (Inference): let the agent return only the body of a proof fn, or only the proof { } blocks and invariant clauses of an executable function, and splice them in mechanically, so that requires and ensures cannot be edited. This is stricter than what Verus needs, since a proof often needs a new helper proof fn; the paper’s Builder cannot add a declaration outside the body. In Lean it can still state a have inside the body, as the Appendix C proof does eleven times.

evidence: none separate.

technique 7: shape the library so proofs avoid index arithmetic

what it is: two definitional choices in the library, and a strict import order.

how it is done (Section 3.1, p.7; Appendix A, p.21):

1. reuse the host language’s list type instead of a new inductive type: “Words are represented as List α rather than a custom inductive type, so that all of Lean’s existing list lemmas and automation are available for free.” (Appendix A, p.21)
2. define sub-word relations by existence of the surrounding pieces, not by positions: “Factor is defined contiguously (IsFactor u w := ∃ x y, w = x ++ u ++ y) rather than via an indexed substring predicate, which keeps proofs by case analysis on x and y direct rather than requiring index arithmetic.” (Appendix A, p.21)
3. build later notions from earlier ones only: a border is the conjunction of proper prefix and proper suffix, and its factor lemma is one application of a Factor lemma (code, p.7)
4. order modules so that “later modules import only earlier ones” (p.7)

Verus form (Inference; a sketch, not run through Verus):

spec fn is_prefix<T>(u: Seq<T>, w: Seq<T>) -> bool {
    exists|s: Seq<T>| w == u + s
}

proof fn prefix_len<T>(u: Seq<T>, w: Seq<T>)
    requires is_prefix(u, w),
    ensures u.len() <= w.len(),
{
    let s = choose|s: Seq<T>| w == u + s;
    assert(w.len() == u.len() + s.len());
}

Seq plays the part of List α, so vstd’s sequence lemmas apply. What changes: an exists in a Verus spec fn needs a trigger and the caller must supply the witness, with choose to take one out and an explicit assert naming one to put one in; Lean’s obtain ⟨x, hw1, hxne⟩ does the first of these in one line (Appendix C, line 5). Inference: for an SMT-backed verifier the existential form is not clearly the easier one, because the solver must find x and y; the paper’s argument is about tactic proofs.

evidence that the choice did not remove index reasoning: the three theorems Kimi K2.6 failed include two that “stemmed from complex modular indexing lookups” (Section 5, p.16), and the period proof still reasons through positions (w.get? i in Appendix C, p.25; Section 5, p.16 speaks of reasoning over List.get? indices). All ten Period theorems are where the weaker backbones fail most: Table 10 (p.24) gives 80.0%, 60.0% and 10.0% for Kimi, Claude Sonnet 4.5 and DeepSeek V4 Pro on Period (8/10, 6/10, 1/10, checked against Table 9).

technique 8: grow the library from solved theorems

what it is: a loop the paper proposes and does not run. Verified proofs are added to the library, after human review, as lemmas for later, harder targets.

how it is done: the paper gives one sentence, no procedure: the suite’s theorems “validate LAMP on a CoW library that did not previously exist, and verified proofs can, after human review, be folded back in to support harder results” (Section 4.1, p.12; part of a longer sentence). Its conclusion counts the possible result: “Folding them back would grow it from 93 to as many as 180 declarations, the kind of compounding foundation LAMP is designed to build as it solves.” (Section 6, p.17) 93 + 87 = 180, checked.

Verus form (Inference): promote a verified helper proof fn into the project’s lemma module and add its record to the ontology of technique 2. Steps not in the paper: deciding which lemmas are worth keeping, and re-running earlier proofs after the library changes.

evidence: none; no experiment uses a grown library.

the example proof and what it shows

Appendix C (p.24–25) gives the one full output: border_period_duality, a border b of w gives w the period w.length - b.length. The 32-line proof (1) unpacks the border into a proper prefix and a proper suffix, (2) obtains w = b ++ x and w = y ++ b with x, y non-empty, (3) proves two length equations with simp and omega, (4) shows the period is positive, (5) for each index i rewrites both w.get? i and w.get? (i + period) to b.get? i. Kimi K2.6 solved it; Claude Sonnet 4.5 and DeepSeek V4 Pro did not (Table 9, #59, p.23).

Verus form (Inference): the same proof is an assert forall|i: int| ... by { ... } over indices, with the two decompositions taken by choose and the length facts as plain asserts that the solver’s linear arithmetic discharges, where Lean needed omega.

all the numbers, with what they are numbers of

• main result, Kimi K2.6, pass@1, 90 theorems (Table 3, p.13): Easy 15/15, Medium 57/58 (98.3%), Hard 15/17 (88.2%)
• pass@1 here means one run of the whole loop, which internally makes up to 9 verification attempts (Section 4.1, p.12)
• backbones inside LAMP, same suite (Table 5, p.14; Table 9, p.22–24): Kimi K2.6 96.7% (87/90), Claude Sonnet 4.5 88.9% (80/90), DeepSeek V4 Pro 68.9% (62/90)
• other systems, same suite, “same ontology context given to every system” (p.14; Table 6): DeepSeek-Prover-V2 7B 8.9% (8/90), Kimina-Prover 7B 3.3% (3/90), Goedel-Prover-V2 32B 1.1% (1/90), backbone LLM without agents 58.9%
• sanity check that Goedel-Prover-V2 works at all: valid proofs on miniF2F for “8B: 6/10, 32B: 2/10” (p.15)
• out of domain, a 32-problem subset of miniF2F, 8 per domain, LAMP with each backbone (Table 7, p.15): Kimi K2.6 96.9%, DeepSeek V4 Pro 56.2%, Claude Sonnet 4.5 34.4% (Inference: 31/32, 18/32, 11/32)
• failure classes for the 38 failure instances of Claude Sonnet 4.5 (10) and DeepSeek V4 Pro (28) together (seven theorems failed under both, so these are not 38 distinct theorems) (Table 8, p.16): incorrect proof strategy 29 (76.3%), invalid Lean syntax 7 (18.4%), ill-posed theorem 2 (5.3%); 29 + 7 + 2 = 38, and the percentages match

Not reported: cost, tokens, wall-clock time per theorem, number of tool calls, how many theorems needed a re-plan.

where the paper disagrees with itself

• the benchmark contains a false statement. “Meanwhile, the failure in primitive_minimal _period_is_length occurred because the theorem statement within the dataset is mathematically false; the multi-agent Planner correctly identified this flaw and refused to generate a proof.” (Section 5, p.16) It is still counted as a failure and kept in every denominator. Inference: on the 89 provable statements Kimi K2.6 scores 87/89 = 97.8%, and the Hard row is 15/16.
• Section 5 (p.16) says of seven theorems failed by both Claude and DeepSeek that they need reasoning “that exceeds current LLM capabilities regardless of backbone choice”. Table 9 lists the seven (#17, #27, #59, #74, #75, #77, #78); Kimi K2.6 solved five of them (#17, #27, #59, #75, #77), and #74 is the false statement. The claim holds for one theorem, #78.
• the text of Section 3.4 cites algorithm lines that are off by one or two from the listing: it says the two checks are at “lines 9 and 14”, the listing has them at 8 and 12–13; it says the fast path is “lines 17–18”, the listing has it at 16–17.
• the abstract says each ablation costs “roughly 12 percentage points”; Table 4 gives 12.3 and 11.1.
• “LAMP is model-agnostic” (Section 4.4, p.14) against the limitations: LAMP is “not a model-agnostic guarantee” (p.17). The spread across backbones is 28 points on CoW and 62.5 points on the miniF2F subset.
• the sanity check for the specialized provers is 2/10 for the 32B model that was then scored 1/90; a prover that solves 2 of 10 in-distribution problems in this harness is weak evidence that the harness ran it properly. Inference: the 1.1%–8.9% figures may partly measure the harness (prompt format, one sample) and not only the missing domain knowledge. The paper defines its metric as pass@1 (Section 4.1, p.12); the sampling budget the provers actually got, and what their own papers use, are not checked here.
• the suite, the difficulty labels and the library are by the same authors who built the system; the paper says so: “The CoW Evaluation Suite is self-constructed, and its difficulty labels reflect our own judgement rather than an external standard; pass rates on it are not directly comparable to established benchmarks.” (Section 5, p.17)

what VL should not redo, and what remains open

Already shown here, for a 93-declaration library in Lean: the backbone model given the same ontology context (Table 6; the paper does not say whether that is the pasted library source) and no agents solves 58.9% of lemmas, and the full agent system adds 38 points; the paper says fine-tuned provers have no mechanism to consume such context (Section 4.4, p.15), which it does not test. Inference: VL need not test again whether pasting the relevant specs and lemma signatures helps; it should take it as the default.

Open after this paper (Inference): whether the ontology adds anything beyond the pasted source (not isolated); whether any of it holds for a library too large to paste; whether it holds when the target is a program with loops, not a list lemma.

threat to VL’s product

Inference: low. The system proves short lemmas about lists in Lean, in a library its authors wrote, with statements its authors wrote, one of them false. It does not write specifications, does not verify programs, and reports no cost. The Planner noticing a false statement is a single observation with one model; the two other backbones did not notice. The parts worth copying are small and generic: the two-gate acceptance check, the mechanical restriction of edits to the proof body, the cheap path for unknown names, and the nested retry budgets.

techniques for the catalog

• import-driven source injection: resolve the target file’s imports and paste the imported library source verbatim into every agent’s prompt, to stop invented lemma names
• domain ontology as a tool: serve per-entity records (statement, description, location, dependencies, related concepts) with family and prerequisite-chain queries, consulted after the pasted source and before general library search
• planner/builder dual loop: a prose plan naming lemmas, up to 3 build attempts per plan with error history, up to 3 plans with a failure summary carried between them
• two-gate acceptance: reject on a text match of the placeholder token, then require a compile with no errors, no placeholders and no placeholder warnings
• missing-definition fast path: on a “name not found” error reload the library context and retry the build without re-planning
• proof-body-only patching: the controller locates the proof region and replaces only it, stripping any re-emitted signature, so the statement cannot change
• existential sub-sequence definitions: define prefix, suffix and factor by the existence of surrounding pieces over the host list type, so proofs split on the pieces instead of on indices
• library growth from solved goals: after human review, add verified proofs to the library as lemmas for harder targets (proposed, not run)

Last edited: 2026-10-13