Several proof assistants provide automation tactics based on tableau-style tree search, such as Isabelle’s and Rocq’s auto and Lean’s Aesop. In this setting we consider forward rules, which apply a given theorem, say, $$A \rightarrow B \rightarrow C$$ , to any goal containing hypotheses A and B, adding C as a new hypothesis. When treated naively, such rules are tried on every goal encountered during the search, leading to repeated unifications of premises A and B with the hypotheses of each goal. We present an approach to forward rules that avoids some of this repeated work by taking advantage of similarities between successive goals. For each goal, we cache partial applications of forward rules in a custom data structure that enables efficient updates. Our technique is compatible with any search strategy and most logics. It has been implemented in Aesop.

White-box proof search tactics such as Coq's auto, Isabelle's auto and Lean's Aesop apply proof rules that often translate directly to lower-level tactics. When these search tactics find a proof, they can, at least in principle, generate a tactic script, i.e. a sequence of lower-level tactics that proves the goal. Such a script can then replace the typically much slower invocation of the search tactic, or it can be used to understand and debug the search. However, at least for Aesop, naively generated scripts are highly unidiomatic. For example, they use tactics that users would typically avoid; they apply these tactics in an unusual order; and they do not use Lean's constructs for structuring tactic scripts. To address these issues, I propose a three-stage optimisation pipeline that transforms naive scripts into scripts resembling a human-written Lean proof. The first stage replaces less idiomatic tactics with more idiomatic ones, checking that the two sequences of tactics produce the same result. The second stage permutes the tactics in the script to bring them into a natural, depth-first order, which then allows us to use Lean's structuring constructs. The third stage runs some straightforward post-processing passes.

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.

In theorem provers based on dependent type theory such as Coq and Lean, induction is a fundamental proof method and induction tactics are omnipresent in proof scripts. Yet the ergonomics of existing induction tactics are not ideal: they do not reliably support inductive predicates and relations; they sometimes generate overly specific or unnecessarily complex induction hypotheses; and they occasionally choose confusing names for the hypotheses they introduce.