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

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

factorized states: split proof state into independent goals

• search is AND-OR tree
  • OR node: choose a tactic
  • AND node: every resulting goal must close
• independent goals can be searched in any order, reused, parallelized
• goals sharing a metavariable stay coupled
  • e.g. Nat.le_trans on 2 ≤ 5 gives 2 ≤ ?m and ?m ≤ 5
  • assigning ?m (e.g. via exact) decouples them
• Verus transfer (inference, untested): independent obligations as separate lemmas with explicit contracts data extraction: normalize existing proofs into small transitions
• 3 stages: singleton-tree construction, tactic simplification, merge metavariable-coupled siblings
• simplification splits cases/induction branches and partitions rw
• whole tree re-executed in Lean REPL, every branch must end proved verifier hygiene
• old Lean REPL accepted 12 incorrect MiniF2F validation proofs without kernel-checking tactic assignments
• apply? behaves like sorry, banned by default
• checks only new assignments per tactic
  • claimed quadratic to linear
• all found proofs rechecked directly by Lean

Last edited: 2026-11-04