Aesop: White-Box Best-First Proof Search for Lean

Jannis Limperg, Asta Halkjær From

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

36 Downloads (Pure)


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. Since we use a best-first search strategy, it is not obvious how to handle metavariables which appear in multiple goals. The most common strategy for dealing with metavariables relies on backtracking and is therefore not suitable for best-first search. We give an algorithm which addresses this issue. The algorithm works with any search strategy, is independent of the underlying logic and makes few assumptions about how rules interact with metavariables. We conjecture that with a fair search strategy, the algorithm is as complete as the given set of rules allows.
Original languageEnglish
Title of host publicationProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs
PublisherAssociation for Computing Machinery
Publication date2023
ISBN (Print)979-8-4007-0026-2/23/01
Publication statusPublished - 2023
Event12th ACM SIGPLAN International Conference on Certified Programs and Proofs - Boston Park Plaza, Boston, United States
Duration: 16 Jan 202317 Jan 2023


Conference12th ACM SIGPLAN International Conference on Certified Programs and Proofs
LocationBoston Park Plaza
Country/TerritoryUnited States
Internet address


Dive into the research topics of 'Aesop: White-Box Best-First Proof Search for Lean'. Together they form a unique fingerprint.

Cite this