A novice-friendly induction tactic for lean. - Jannis Limperg (CPP, 2021)

Aesop: White-Box Best-First Proof Search for Lean. - Jannis Limperg; Asta Halkjær From (CPP, 2023)

Tactic Script Optimisation for Aesop. - Jannis Limperg (CPP, 2025)