Automated Discovery of Tactic Libraries for Interactive Theorem Proving

Watch this 11-minute conference presentation from OOPSLA 2025 that introduces a novel approach to automatically discovering tactic libraries for interactive theorem proving systems. Learn about Tactic Dependence Graphs (TDGs), a new method that captures logical dependencies between tactic applications while abstracting away syntactic details to identify reusable proof strategies across multiple proofs. Discover how the TacMineR tool implements this technique and outperforms existing anti-unification-based approaches like Peano by learning 3× more tactics and reducing proof sizes by 26% across benchmarks. Explore the practical benefits of custom tactic learning for proof automation, including how it enables state-of-the-art automation tools to achieve a 172% relative increase in success rates. The presentation covers the theoretical foundations of TDGs, the implementation details of TacMineR, comprehensive evaluation results comparing against existing methods, and demonstrates applications in popular interactive theorem provers such as Rocq and Lean. Gain insights into how this research advances formal reasoning by enabling more concise and modular proofs through automated tactic discovery and proof refactoring techniques.