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

Limperg, J; From, AH

Limperg, J (通讯作者),Vrije Univ Amsterdam, Dept Comp Sci, Amsterdam, Netherlands.

PROCEEDINGS OF THE 12TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2023, 2023; (): 253

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 pro......

Full Text Link