Lean Graph Search for Formal Theorem Proving

• Multi-hop dependencies can uncover supporting lemmas that have little lexical similarity to a query but recur in proofs of related problems.Existing retrieval systems focus on declarations relevant to a target theorem or intermediate goal, with limited use of these dependencies.Source: §1 · p. 1
• Recall@100 rose from 82.7% with LeanSearch v2 (Gao et al., 2026) to 94.7% on MathlibQR’s 810-query fair subset.The result is reported for the fair subset of MathlibQR.Source: Figure 1 · p. 2, §1 · p. 2
• On MathlibMPR (Gao et al., 2026), Covered@20 rose from 39.1% to 42.8% and Covered@50 from 41.3% to 44.2%.These are proof route-level premise coverage results.Source: Figure 1 · p. 2, §1 · p. 2
• LEANGRAPHSEARCH builds a directed graph from Mathlib’s forward dependencies, seeds personalized PageRank with semantically retrieved declarations, then reranks expanded candidates against the query.The graph links each declaration to premises it directly depends on; graph scores are combined with second-pass query relevance scores for final ranking.Source: §1 · p. 2
• Integrated into an iterative proving loop with Lean diagnostic feedback and problem-local failure memory, LEANGRAPHSEARCH consistently outperforms retrieval baselines across three theorem-proving benchmarks.The benchmarks are FATE-H (Jiang et al., 2026), MathlibMPR-Prop (Gao et al., 2026), and Lean-IMO-Bench (Kung et al., 2026).Source: §1 · p. 2

Background

• LLM-based formal proving includes generating tactics during proof-state search and refining proof scripts through verifier feedback, often guided by informal proof sketches.Here, mathematical search means retrieving library declarations for formal proving using informal or formal queries.Source: §2 · pp. 2–3

Search for Formal Mathematics

• Prior formal-math search retrieves reusable library facts through premise selection, retrieved-premise tactic generation, context-specific and proof-state search, semantic declaration search, and global proof retrieval.The approaches include contrastive training and reranking, intent-aware embeddings, and iterative sketch–retrieve–reflect cycles.Source: §2 · p. 3

Graph-based Retrieval

• Graph retrieval uses knowledge-graph expansion and, in formal libraries, declaration dependencies for descriptions, centrality ranking, bottom-up descriptions, and graph-aware premise representations.Examples include personalized PageRank for multi-hop retrieval and a relational graph neural network over state–premise and premise–premise dependencies.Source: §2 · p. 3

3.1 TASK FORMULATION

• Retrieval queries may be informal descriptions, Lean statements, proof states, or combinations, and can seek either a matching declaration or premises supporting a complete proof.A proving problem has one Lean proof hole; queries may use the source, a prior candidate, or compiler diagnostics.Source: §3.1 · pp. 3–4

3.2 DECLARATION DEPENDENCY GRAPH CONSTRUCTION

• Static analysis with jixia builds a directed graph whose edges point from each Mathlib declaration to declarations referenced in its type or value.Traversing these links can surface shared supporting declarations even when their surface forms differ, complementing semantic similarity without changing Mathlib.Source: §3.2 · p. 4

3.3 GRAPH-BASED RETRIEVAL

• Embedding–reranker matches seed query-specific personalized PageRank over dependencies; LeanGraphSearch merges the expanded candidates with seeds and reranks them against the original query.The restart term anchors propagation to the seed distribution while graph transitions expand toward dependencies.Source: §3.3 · pp. 4–5, Figure 2 · p. 4

3.4 SEARCH LOOP POLICY

• Standard Mode invokes graph retrieval after a failed proof attempt using the current proof state, while Reasoning Mode also decomposes the theorem into queries before the first attempt.Reasoning Mode aggregates evidence across subqueries and truncates it to K declarations.Source: §3.4 · p. 5

4.1 SETUP

• Evaluation uses MathlibQR’s 810-query fair subset and 69 MathlibMPR theorems, measuring nDCG@k, Recall@k, Recall@k (group), and Covered@k; reasoning-mode results average two backbone models.The backbones are Gemini 3.1 Pro and Claude Sonnet 5; comparisons include non-agentic and agentic search methods and methods queried with current proof states.Source: §4.1 · pp. 5–6

4.2 RESULTS

• On MathlibQR, nDCG@10 rises from 0.616 to 0.629, Recall@50 by 7.8 percentage points, and Recall@100 by 12.0; on MathlibMPR, Covered@20 and Covered@50 improve by 3.7 and 2.9 points.Group recall improves at four of five cutoffs, with Recall@10 the exception.Source: Table 1 · p. 6, Table 2 · p. 6, §4.2 · p. 6
• On MathlibQR, graph-aware expansion connects semantic matches such as constructors and projections to underlying declarations missed because their names and signatures are less lexically similar.The connections follow dependency relationships among declarations.Source: §4.2 · p. 6
• On MathlibMPR, LeanGraphSearch retrieves more gold declarations in the top five despite returning fewer filtered declarations on average, concentrating relevant premises and improving group recall and complete-route coverage.Route-level examples illustrate this context-composition effect.Source: §4.2 · p. 6

5.1 LEANGRAPHSEARCH IN AN AGENTIC PROVING LOOP

• The agentic loop revises a single candidate lineage using Lean compiler feedback and can retrieve declarations from five queries after a failed attempt.Optional failure memory records recurring formal failure states and returns dead-end records and failed modifications to encourage alternative repairs.Source: §5.1 · p. 7

5.2 SETUP

• Evaluation uses FATE-H, MathlibMPR-Prop, and Lean-IMO-Bench, with at most 32 reflection turns and pass@k reported for k = 8, 16, and 32.The study compares LeanGraphSearch with LeanSearch v2 and the vanilla backbone LLM without retrieval; Gemini 3.1 Pro is used throughout, with five queries of up to 50 declarations per retrieval action.Source: §5.2 · pp. 7–8

5.3 RESULTS

• 136 to 143 problems solved within 32 turns without memory (and 134 to 142 with memory) as Standard-Mode LeanGraphSearch beats LeanSearch v2 across all sets.Reasoning-Mode LeanGraphSearch achieves the highest total solved count, with particularly strong results on FATE-H.Source: Table 3 · p. 8, Table 4 · p. 8, §5.3 · p. 8
• 69 versus 61 FATE-H problems are solved within 16 turns without memory, while Reasoning-Mode LeanGraphSearch with memory solves 75 within 16 turns versus 73 for LeanSearch v2 within 32.At k = 8, failure memory increases solved counts from 106 to 111 for Standard-Mode LeanGraphSearch and from 99 to 105 for Standard-Mode LeanSearch v2; LeanGraphSearch's Reasoning-Mode aggregate pass@16 rises from 132 to 138.Source: §5.3 · pp. 8–9
• Standard-Mode LeanGraphSearch achieves the lowest API cost per solved problem, while Reasoning Mode with memory solves 151 of 210 at lower cost per solved problem than LeanSearch v2.The qualitative analysis attributes retrieval gains to following multi-hop dependencies to find supporting premises that direct query matching may miss.Source: Figure 3 · p. 9, §5.3 · p. 9

6 CONCLUSION

• The method propagates relevance from semantically relevant declarations along Mathlib dependency edges with personalized PageRank, then reranks expanded candidates against the original query.The conclusion reports improvements in declaration recall and annotated proof-route coverage.Source: §6 · p. 9
• LeanGraphSearch improves proof completion over matched LeanSearch v2 configurations on most evaluated benchmarks and reflection budgets, while reducing aggregate API cost per solved problem.The conclusion attributes these gains to guidance from formal-library dependencies in retrieving premises needed for proof construction.Source: §6 · p. 10

AI USE STATEMENT

• The authors used generative AI to implement methods, assist with translation, create or edit code, analyze literature, and source or search for information.They state that these uses did not include proposing hypotheses, designing or interpreting experiments, formulating mathematical claims, or assisting in writing proofs.Source: AI USE STATEMENT · p. 10
• The authors state that at least two authors double-checked all code, writing, and references, and that they take responsibility for the final content and AI-assisted artifacts.Source: AI USE STATEMENT · p. 10

ETHICS STATEMENT

• The authors describe the work as formal mathematical declaration search and theorem-proving harness research, with no societal consequences they felt required specific highlighting.Source: ETHICS STATEMENT · p. 10

REPRODUCIBILITY STATEMENT

• The authors state that the models and data are accessible online, baselines are cited, and a redacted codebase is available as supplemental material.They point readers to Gao et al. (2026) and frenzymath (2024) codebases for reproducing the framework, and to the Appendix for implementation details.Source: REPRODUCIBILITY STATEMENT · p. 10

A.1 RETRIEVAL TASKS AND BENCHMARKS

• General retrieval benchmarks span heterogeneous domains, representation tasks, reasoning beyond semantic matching, and natural-language or statement-level mathematical search.Examples include BEIR, MTEB, BRIGHT, NaturalProofs, and Matlas.Source: §A.1 · p. 15
• MathlibQR evaluates retrieval for individual target declarations, while MathlibMPR measures premise-group coverage across alternative complete proof routes.The evaluation combines these retrieval measures with downstream proof completion.Source: §A.1 · p. 15

A.2 FORMAL THEOREM-PROVING SYSTEMS

• Premise-selection systems connect mathematical libraries to automated reasoning through proof reconstruction, learned premise ranking, and stepwise tactic search.Examples include Sledgehammer, CoqHammer, Thor, Magnushammer, HOList, HyperTree Proof Search, ReProver, and REAL-Prover.Source: §A.2 · p. 15
• Recent prover work uses mathematical pretraining, synthesized data, self-correction, reinforcement learning, and informal reasoning to guide formal proof generation.The experiments hold the prover fixed to isolate how access to library declarations affects proof completion.Source: §A.2 · p. 15
• Unlike prior dependency-aware representations, LeanGraphSearch traverses dependencies conditioned on the query to expand candidates for semantic reranking.Related work also uses verified-lemma retrieval and dependency information during autoformalization.Source: §A.2 · p. 15
• An optional failure memory associates unsuccessful repairs with recurring formal failure states, complementing retrieved library evidence during proof construction.This contrasts with approaches that use unsuccessful tactics or reflections on failed attempts to guide search.Source: §A.2 · p. 15

• Formal proving benchmarks span competition mathematics, formalized undergraduate problems, and collections focused on mathematical domains and difficulty levels.Examples include miniF2F, FIMO, PutnamBench, ProverBench, ProofNet, Formal-MATH, CombiBench, FATE, and MA-ProofBench.Source: §A.3 · pp. 15–16
• Context- and structure-focused benchmarks include miniCTX for proving in real Lean projects and TheoremBench for progress through supporting subtheorems.The authors evaluate proving on FATE-H, MathlibMPR-Prop, and Lean-IMO-Bench, covering graduate algebra, Mathlib developments, and Olympiad problems.Source: §A.3 · p. 16
• Together with MathlibQR and MathlibMPR, the proving benchmarks connect declaration retrieval and premise coverage to proof completion under different reflection budgets.Source: §A.3 · p. 16

B IMPLEMENTATION DETAILS

• The implementation graph contains 310,579 declarations and 4,528,330 forward dependency edges, with self-references, duplicates, and references to absent targets removed.The dependency-only profile uses unit-weight forward edges; theorem proof-body references are configurable at graph-construction time.Source: §B.1 · p. 16

B.1 RETRIEVAL BACKEND AND DEPENDENCY GRAPH

• LeanGraphSearch uses 50 semantic seeds and 200 PPR-ranked expansion candidates, but returns at most 50 declarations per query, matching LeanSearch v2’s output budget.PPR uses restart probability 0.15, at most 50 iterations, and an ℓ1 convergence tolerance of 10^-6; the refined candidate pool is capped at 100 declarations.Source: §B.1 · p. 16
• Before a second reranking pass, the implementation merges first-pass semantic and PPR-ranked candidates, then applies a graph-aware prefilter combining min–max-normalized semantic and PPR scores with a log-degree penalty.Defaults are α = β = 1 and γ = 0.05; graph-only candidates receive initial semantic score zero. The final PPR z-score correction uses λ = 0.005, with mean and standard deviation computed over retained candidates for the current query; zero-variance PPR contributes zero correction.Source: §B.1 · pp. 16–17

B.2 SEARCH LOOP POLICY

• The reasoning controller decomposes the statement into definition, high-level-result, and proof-step queries, filters candidate declarations, and asks a judge whether they support the plan.If rejected, the plan and judge feedback inform another decomposition call; independent branches run concurrently, with the first accepted plan used or completed branches pooled otherwise.Source: §B.2 · p. 17
• Standard Mode begins without retrieved context and requests five queries after a failed proof attempt, deduplicating up to 250 returned entries before supplying them to the prover.Reasoning Mode starts with an adaptive reasoning context and can trigger the same reflection-time queries after failures; the GET QUERY INIT template is not used in the five evaluated configurations.Source: §B.2 · p. 17

B.3 MATHEMATICAL RETRIEVAL SETTING

• MathlibQR evaluation uses 810 queries from the shared-declaration subset and compares each retriever’s final top 200 declarations, retaining K = 50 and N = 200 for LeanGraphSearch.Recall@k indicates whether the single annotated target appears within the first k results, while nDCG@k discounts its rank logarithmically; metrics are averaged across queries.Source: §B.3 · pp. 17–18
• MathlibMPR supplies the formal statement and NL main-result description to a two-branch reasoning driver, then measures macro-averaged group recall and complete route coverage at k = 5, 10, 20, 30, and 50.Covered@k checks complete coverage of the original or annotated alternative route; reported results are averaged over Gemini 3.1 Pro and Claude Sonnet 5.Source: §B.3 · p. 18

B.4 THEOREM PROVING SETTING

• The evaluation uses 100 FATE-H problems, 50 selected MathlibMPR entries, and 30 problems from each Lean-IMO-Bench difficulty level, with Gemini 3.1 Pro as prover.Temperature is set to zero for proof generation, query generation, and reasoning-controller calls; each revision uses the current candidate, latest diagnostic, and available retrieval and failure-memory context.Source: §B.4 · p. 18
• Lean success requires valid protected source boundaries and successful elaboration without unresolved sorry obligations.The checker rejects changes to the target proof hole’s immutable context, additional top-level commands, and prohibited constructs; verification uses lean-interact with Mathlib and a 600-second default timeout.Source: §B.4 · p. 18
• Completion is measured cumulatively at 8, 16, and 32 reflection rounds, while proof-generation calls, retrieval actions, and compiler submissions are tracked separately.One retrieval action may issue several queries, and initial reasoning preparation has a separate planning budget; counters distinguish new compilations from candidates rejected using cached feedback.Source: §B.4 · p. 18
• Per-problem failure memory records stable failed candidates and their diagnostics, unresolved goals, context, inferred failing tactic, identifiers, and nearby source snippet.A SHA-256 hash identifies each state; after two observations, feedback can include up to three recurrent states and three recent failed edits per state, directing the prover to change the unsuccessful repair.Source: §B.4 · pp. 18–19
• When enabled, failure-memory guidance and summaries reach proof-refinement and reflection-query prompts, treating failed tactics as context-specific rather than globally prohibited.A corrected application may remain valid after its arguments, goal, instances, or local hypotheses change; repeated states trigger a DEAD END REPEATED directive.Source: §B.4 · pp. 18–19
• Cached deterministic failures are rejected without recompilation, while cached retrieval queries reuse results and prepared retrieval context is retained for replacement candidates.Infrastructure failures are excluded from the stable-failure cache, and generation calls for rejected candidates still count toward model usage.Source: §B.4 · p. 19
• API expenditure counts paid proof-generation, query-generation, and reasoning-based retrieval calls, including calls on unsuccessful problems, and is normalized against no retrieval within each benchmark and memory setting.Local retrieval and Lean-verification hardware costs are excluded; retained results include proof attempts, diagnostics, retrieval traces, and available usage and memory statistics.Source: §B.4 · p. 19

C.1 MATHEMATICAL RETRIEVAL

• Type-reference edges connect retrieved constructors to underlying mathematical objects that LeanSearch v2 misses from its top 100.LEANGRAPHSEARCH ranks CategoryTheory.NatTrans third, Matroid second, and HomotopicalAlgebra.ModelCategory first via NatTrans.mk, Matroid.mk, and ModelCategory.mk’, respectively.Source: §C.1 · p. 19
• Value references in declaration bodies recover relevant targets from weak semantic matches, including presheafed spaces, schemes, and natural transformations.The recovered targets rank fourth for AlgebraicGeometry.PresheafedSpace, eighth for AlgebraicGeometry.Scheme, and 14th for CategoryTheory.NatTrans; each is outside LeanSearch v2’s top 100.Source: §C.1 · p. 19
• Top-five retrieval completes MathlibMPR Query 15’s two-premise route, while Query 75’s filtered context concentrates cover-lifting and adjunction-naturality steps.For Query 15, the two lemmas move from LeanSearch v2 ranks 1 and 7 to LEANGRAPHSEARCH ranks 1 and 4. For Query 75, cover lift moves from rank 18 to 2, superset covering from rank 8 to 3, and both adjunction hom-equivalence naturality lemmas enter the filtered list at ranks 21 and 15.Source: §C.1 · pp. 19–20

C.2 THEOREM PROVING

• LeanGraphSearch solves several problems within budgets or in fewer reflection rounds than LeanSearch v2, with lower API costs in reported cases.It succeeds at round 10 on MathlibMPR-Prop Problem 51 and FATE-H Problem 88 when LeanSearch v2 exhausts its budget; on MathlibMPR-Prop Problem 34, both solve the problem, but LeanGraphSearch finishes at round seven rather than 16 and costs $3.25 rather than $8.33. Per-attempt API cost also falls on MathlibMPR-Prop Problem 34 from $0.490 to $0.406, FATE-H Problem 15 from $0.572 to $0.415, and Lean-IMO-Bench Advanced Set Problem 25 from $0.543 to $0.416.Source: §C.2 · p. 20
• Failure memory helps LeanGraphSearch recover from repeated failures and finish proofs sooner, including one problem the no-memory run leaves unsolved.On Lean-IMO-Bench Basic Set Problem 16, memory records a repeated recursion-depth failure and the run succeeds at round nine; on FATE-H Problem 12, it reduces completion from round 30 to seven and API cost from $17.26 to $4.56. The memory is initially empty and supplies structured failure summaries to revision and reflection-time query generation.Source: §C.2 · p. 20, §D.1 · p. 21

D.1 PROMPT INTERFACES

• The prompt interfaces combine route planning and retrieval with compiler-feedback-driven proof revision, while requiring generated tactic bodies to preserve the fixed theorem context.Reasoning retrieval plans, filters up to 50 declarations per query, and judges whether premises support an implementable route; Standard Mode starts without retrieved context, while Reasoning Mode begins with a sketch and premises. After failures, both can retrieve using five complementary queries, and Lean diagnostics guide later revisions.Source: §D.1 · p. 21

D.2 DECODING AND SEARCH BUDGETS

• Matched comparisons use shared prompt templates and model settings, with retrieval outputs capped at 50 declarations and proving trajectories limited to 31 revisions.LeanGraphSearch expands 200 PPR-ranked candidates internally without increasing the per-query output budget; proof-stage query and generation calls share a 63-call budget.Source: §D.2 · pp. 21–22

D.3 INSTANCE SELECTION AND ACCOUNTING

• Retrieval uses a fixed fair MathlibQR subset and all MathlibMPR instances, while proving evaluates one trajectory per problem and reports cumulative pass@k and API expenditure.The proving sets contain 50 MathlibMPR-Prop propositions, 100 FATE-H problems, and 30 problems from each Lean-IMO-Bench set; pass@32 is the full-budget result, and API cost includes model calls but excludes local retrieval and compilation.Source: §D.3 · p. 22

D.4 REASONING RETRIEVAL PROMPTS

• The shared reasoning-retrieval prompts support MathlibMPR retrieval and initial reasoning retrieval for theorem proving.The reasoning procedure uses planning, retrieval, filtering, and route assessment; two branches may revise plans using judge feedback, and the first accepted route is selected.Source: §D.1 · p. 21, §D.4 · p. 22

D.4.1 INITIAL ROUTE GENERATION.

• Initial route generation asks for high-level theorems, definitions, and stepwise lemmas, with concrete proof decomposition and no more than 20 queries.The prompt emphasizes using the informal proof, specifying constructions and type boundaries, and retaining detailed fallback steps if high-level results are not found.Source: §D.1 · p. 21, §D.4.1 · pp. 22–23

D.4.2 ROUTE REVISION AFTER JUDGE FEEDBACK.

• After judge rejection, route revision requests a fundamentally different proof plan while preserving the informal proof’s overall narrative.The prompt encourages alternative proof structures and mathematical pathways, including shifting between direct calculation, high-level theorems, and constructive approaches.Source: §D.4.2 · pp. 24–25
• Route revision requests core definition queries, 2–4 distinct high-level approaches, and a structurally different step-by-step proof, with no more than 20 total queries.The revised plan should focus on theorems that Lean can easily verify.Source: §D.4.2 · p. 25

D.4.3 PER-QUERY RELEVANCE FILTERING.

• Per-query filtering keeps results only when their mathematical concept, type signature, and applicable algebraic structures match the target, returning an empty list when no direct match exists.It excludes mismatched, tangential, auxiliary, or redundant results and asks for reasoning about kept and rejected items, especially type mismatches.Source: §D.4.3 · pp. 26–27

D.4.4 ROUTE-QUALITY ASSESSMENT.

• Route-quality assessment judges each proof step for soundness, verifiability, Lean implementation difficulty, and support from retrieved theorems, flagging missing coverage or steps that need decomposition.The assessment focuses on implementation complexity rather than mathematical elegance and considers whether available results and simple tactics can resolve each step.Source: §D.4.4 · p. 27

D.5 THEOREM-PROVING PROMPTS.

• The theorem-proving prompts share integrity rules and provide immutable source context, retrieved declarations, the previous tactic body, compiler feedback, and optional failure-memory guidance.Failure-memory guidance is empty when memory is disabled and contains the Section D.6 instruction when enabled.Source: §D.5 · p. 28

D.5.4 REFLECTION-TIME RETRIEVAL QUERIES.

• Reflection-time retrieval asks for exactly five distinct natural-language queries grounded in the target, failed tactic, and compiler feedback, describing the missing fact or API and relevant types or hypotheses.Queries should avoid repeated paraphrases, may include definitions or bridge lemmas, and should not assume a benchmark answer; a failed application does not invalidate every use of that lemma.Source: §D.5.4 · p. 31

D.6.1 CONTEXTUAL FAILURE-MEMORY GUIDANCE.

• Failure memory treats prior tactic or declaration failures as evidence about that application, not a global ban, and encourages revised arguments or alternative strategies.When a formal state recurs at least twice, feedback says not to repeat the same tactic, lemma, declaration, or proof modification; Lean checks the submitted proof.Source: §D.6.1 · pp. 31–32

D.6 FAILURE-MEMORY PROMPT AND FEEDBACK

• Failure-memory feedback records unsuccessful applications and recurrent formal states, and is supplied to both proof revision and reflection-time query generation.When memory is enabled, its instruction is inserted verbatim into the initial proof prompt and every proof-revision prompt, but not standalone MathlibMPR retrieval.Source: §D.6 · p. 31, §D.6.1 · p. 32

D.5.1 SHARED PROOF-INTEGRITY RULES.

• Proofs must use the target’s hypotheses and existing Mathlib facts, avoid unproved assumptions and trusted-code escapes, and prove any helper claims locally.The host owns top-level declarations and immutable source boundaries; candidates are checked by Lean, and rejected proofs return feedback rather than counting as successes.Source: §D.5.1 · p. 28

D.5.2 INITIAL PROOF ATTEMPT.

• Treat search results and reasoning sketches as candidates: verify declarations’ types and assumptions, adapt mismatched routes, and never invent facts or assumptions.Search rank or informal similarity does not establish applicability, and empty results do not show that a needed Mathlib fact is absent.Source: §D.5.2 · p. 29
• Construct the initial proof by matching the exact goal and hypotheses, applying a suitable library result or reducing the goal with explicit intermediate claims.Use local helper proofs and ordinary tactics, while matching coercions and typeclass assumptions at each application.Source: §D.5.2 · p. 29
• The initial response supplies a concise plan and one code block containing the complete tactic body, without repeating or modifying host-owned source.The prefix already ends in `:= by`; the suffix and theorem context remain immutable, and helpers belong inside the tactic body.Source: §D.5.2 · p. 29

D.5.3 PROOF REVISION AFTER FEEDBACK.

• After failure, use compiler feedback to prioritize the earliest syntax or scope error, then repair structure, types, coercions, instances, or the displayed goal as appropriate.For unknown identifiers, distinguish local-name, namespace, and library issues; preserve working proof parts, but change strategy when progress stalls.Source: §D.5.3 · p. 30
• If feedback identifies an integrity violation, remove the offending construction and prove any useful helper locally before completing the original target.Return a brief obstacle-and-repair note followed by the entire repaired tactic body, not a patch, while leaving the host’s prefix and suffix untouched.Source: §D.5.3 · p. 30