Papers With

← All papers
cs.LO

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

Jannis Limperg, Asta Halkjær From

cs.LO Jan 16, 2023 · v1
tactic-automation tooling
Read PDF arXiv abstract
TL;DR
Implements a configurable white-box best-first proof search tactic for Lean 4.
Abstract
Aesop is a proof search tactic for the Lean 4 proof assistant. It applies a configurable set of rules using best-first search to try to close a goal. Unlike black-box automation tactics, Aesop is designed to be transparent and predictable: users can inspect the search tree to understand why a proof succeeded or failed, and can control the search by adding or removing rules. Aesop supports safe and unsafe rules with configurable priorities, norm rules for simplification, and can unfold definitions during search.
Problem

Lean 4 needs a transparent, configurable proof search tactic that allows users to understand why proofs succeed or fail and to control the search process, unlike black-box automation tactics.

Approach

Aesop implements white-box best-first proof search for Lean 4 with a configurable set of rules. It supports safe and unsafe rules with configurable priorities, norm rules for simplification, and can unfold definitions during search. Users can inspect the search tree to understand proof outcomes and control search by adding or removing rules.

Results

Aesop provides transparent, predictable proof automation for Lean 4 that has become part of the standard Lean/Mathlib toolchain, offering users visibility into the search process while maintaining effective automation.