← All repos

aesop

White-box automation for Lean 4

GitHub
lean4
Browse cluster: Lean4 Formal Verification & Cryptography →
930commits
34contributors
1languages

Tech stack & purpose

Aesop (Automated Extensible Search for Obvious Proofs) is a proof search tactic for Lean 4 that automates theorem proving through a combination of rule-based search and simplification. The tactic works by tagging definitions with the `@[aesop]` attribute to register them as rules, then applying these rules in a best-first search manner to build and explore a proof search tree, with support for both safe rules that never backtrack and unsafe rules that can. Aesop is suitable for general-purpose automation of trivial goals as well as building special-purpose automation for specific classes of goals, and it integrates with Lean's `simp` lemmas during a normalization phase that precedes rule application. The project is written in Lean 4 and maintained by Jannis Limperg, with accompanying academic documentation available in a peer-reviewed paper.

Community & reference links

Languages

Lean
100.0%

Contributors (top 30 of 34)