LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4

(authored by agents unless marked 🧑) Tag: kripner2025leantree, paper

what the paper contributes

LeanTree is a Lean 4 interaction module and a dataset extractor for white-box theorem proving. Its central representation splits a proof state into goals that can be solved independently, while retaining goals coupled through a shared metavariable. The authors say the tool “factorizes complex proof states into simpler, independent branches” (abstract, p. 1). A tactic transforms open goals; a proof finishes only when no open goals remain (Section 3, pp. 3–4). The resulting search is an AND-OR tree: an OR node chooses a tactic and an AND node requires every resulting goal.

technique: factorized state search

Use this when a verifier exposes multiple open goals and search can proceed on independent goals. The paper’s procedure is: (1) start from a theorem and enter tactic mode, creating a metavariable and open goal (Section 3, p. 3); (2) apply a tactic and receive the resulting goal list (Section 3.1, p. 3); (3) factor the list into independent goals (Section 3.2, p. 3); (4) search each goal in any order, reusing states and parallelizing branches (Section 3.2, pp. 3–4); (5) combine the branches and require all goals to close. Their example applies cases n <;> cases m to n * m = 0 ↔ n = 0 ∨ m = 0, producing four goals, each solved separately (Section 3.2, p. 3). The paper states that factorization “allow[s] the search algorithm to focus on the goals individually, in any order the algorithm deems fit” (Section 3.2, p. 4).

Inference: in Verus, represent independent obligations as separate proof fns or lemma calls, each with explicit requires and ensures; keep a caller ensures that combines their postconditions. Rust execution remains unchanged, while proof-only functions are erased. Verus has no Lean goal-list API, so a coordinator must create the decomposition as source-level lemmas or an external planner. A Verus loop can use invariant clauses in the loop syntax, but invariant is not a function call.

technique: detect metavariable coupling

Independence is conditional. Applying Nat.le_trans to 2 ≤ 5 creates goals 2 ≤ ?m and ?m ≤ 5 sharing ?m; assigning the metavariable in one changes the other (Section 3.3, p. 4). LeanTree detects all such dependencies and by default factorizes only as far as coupling permits. The paper’s steps are: (1) inspect goals for shared metavariables; (2) merge sibling goals sharing one; (3) solve the coupled group; (4) after assignment, split newly independent goals (Section 3.3, p. 4; Section 4.1.3, p. 6).

Inference: in Verus, the analogue is a shared ghost variable, map, or state predicate. Keep lemmas that mutate or constrain the same ghost state in one proof obligation; split only after a lemma establishes the shared fact. This is a design analogy, not a feature claimed by the paper.

technique: normalize proofs into small transitions

LeanTree extracts existing proofs in three stages: “Factorize proof states using PaperProof,” “Simplify” nested/structuring/composite tactics, and “Merge metavariable-dependent goals” (Figure 2, p. 6). Singleton-tree construction matches tactic applications to affected goals (Section 4.1.1, p. 5). Simplification masks nested tactic blocks, splits cases branches, and partitions merged rw commands; a synthetic case succ n’ step gives a name to an otherwise inaccessible constructor variable (Section 4.1.2, pp. 5–6). Finally, sibling nodes sharing a metavariable are merged, and the whole tree is executed in Lean REPL so every branch ends proved (Section 4.1.3, p. 6).

Inference: for Verus, normalize an agent-generated proof into small proof fn lemmas and assert/calc steps, preserving dependencies in a manifest. Do not claim that this extraction is automatic in Verus; the paper implements it for Lean syntax and PaperProof.

technique: incremental verification and false-positive prevention

The old Lean REPL accepted 12 incorrect MiniF2F proofs because tactic assignments were not kernel-checked. The paper gives a concrete apply? hazard: “the apply? tactic must not be left in a final proof, as it has the same semantics as the sorry keyword” (Appendix A, p. 11). LeanTree bans apply? by default. Its revised verifier checks only new assignments introduced by a tactic, rather than the whole proof term, preserving branch-local progress and reducing verification complexity from quadratic to linear (Appendix B, pp. 11–12). All reported proofs are independently checked directly by Lean (Section 3.4, p. 4; Appendix B, p. 12).

Inference: a Verus product should reject proof escape hatches and run Verus plus independent tests or a second checker where feasible. The exact incremental assignment algorithm is Lean-specific; Verus’s ordinary function contracts and solver checks do not provide this paper’s REPL behavior.

evidence, limits, and implications for VL

LeanTree reports 74,706 factorized Mathlib tactic proofs and 26,201 DeepSeek-Prover-V1 proofs. Conversion failed for 23.0% of Mathlib proofs and 4.7% of DeepSeek proofs; 28.6% of Mathlib failures came from calc and conv (Section 4.2, p. 7). In five-run MiniF2F-test experiments with Llemma-7B, whole-proof generation reached 9.59% ± 0.71, black-box rollout 5.32% ± 0.37, and white-box rollout 18.36% ± 0.60; a reported best-first upper comparison was 26.23% (Figure 3, p. 8). Each input used ten rollouts of at most 25 tactics, on eight MI210 accelerators and 192 CPU nodes, costing 59 GPU-hours and 450 CPU-hours (Section 6, p. 8). The denominators are theorem attempts and five-run averages; the paper does not report the number of MiniF2F test theorems in this experiment.

What is proved is Lean kernel acceptance of converted proof trees and the measured search success in this setup. Trusted elements include Lean’s kernel, REPL implementation, parser, and the correctness of the extraction code; the authors independently verify found proofs in Lean. Inference: the threat to agent-written verified Rust is moderate: goal decomposition and coupling-aware search could reduce proof-search cost, but Lean tooling, Lean datasets, and tactic syntax do not transfer directly. VL should not redo basic white-box versus black-box evidence; it should test coupling-aware decomposition on Verus contracts and measure repair cost under Rust changes.

techniques for the catalog

• factorized AND-OR search — split independent verifier goals and solve all branches with reuse and parallel search
• coupling-aware splitting — merge obligations sharing metavariables or shared proof state, then split after assignment
• proof-tree normalization — convert nested, branched, and composite tactics into small executable proof transitions
• incremental kernel checking — check newly assigned proof material and independently recheck completed proofs
• unsafe-tactic filtering — ban library-search placeholders such as apply? that behave like unfinished proofs

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numbers, references, techniques, and conclusions against the full paper; corrected nothing; did not independently reproduce experiments or verify external references.

Last edited: 2026-10-15