Aesop: White-Box Best-First Proof Search for Lean
Jannis Limperg, Asta Halkjær From
Abstract
We present Aesop, a proof search tactic for the Lean 4 interactive theorem prover. Aesop performs a tree-based search over a user-specified set of proof rules. It supports safe and unsafe rules and uses a best-first search strategy with customisable prioritisation. Aesop also allows users to register custom normalisation rules and integrates Lean's simplifier to support equational reasoning. Many details of Aesop's search procedure are designed to make it a white-box proof automation tactic, meaning that users should be able to easily predict how their rules will be applied, and thus how powerful and fast their Aesop invocations will be.
Topics & Concepts
Computer scienceSet (abstract data type)Automated theorem provingWhite boxTree (set theory)Meaning (existential)Programming languageProof assistantAutomationTheoretical computer scienceGas meter proverSoftware engineeringMathematical proofMathematicsEngineeringMathematical analysisPsychologyPsychotherapistMechanical engineeringGeometryLogic, programming, and type systemsFormal Methods in VerificationSoftware Engineering Research