Aesop: White-Box Best-First Proof Search for Lean
summary
Aesop is a white-box proof-search tactic for Lean 4 that runs a tree search over user-registered rules and prioritises goals by best-first with per-rule success probabilities so likely paths get explored first. It layers fixed-point normalization (including Lean’s simplifier and mathlib simpsets), a safe-rule phase that marks goals done, and an unsafe search phase. Core contribution: an algorithm handling metavariables by cloning goals to defer instantiations, conjecturally complete under fair search; practical caveats are heavy copying and potential performance costs.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 0:56Outline
- 1:12Basic Approach
- 2:25BestFirst Search
- 5:30Extensions
- 5:59Normalization
- 9:11Safe Rules
- 10:52Unsafe Rules
- 19:15Questions
related talks
24mTowards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by(…)
22mAutomate your inner scout
22mTowards general white-box automation: a typeclass-guided context cleaner
19mQED in Context: An Observation Study of Proof Assistant Users
01h 10mMedium-scale automation for proof assistants
15mAdaptable Traces for Program Explanations
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
56mMy Journey to the Dark Side: Under-Approximation, Incorrectness, Proof