Noah Goodman

Automated Discovery of Tactic Libraries for Interactive Theorem Proving

2025 · arXiv (Cornell University)

Enabling more concise and modular proofs is essential for advancing formal reasoning using interactive theorem provers (ITPs). Since many ITPs, such as Rocq and Lean, use tactic-style proofs, learning higher-level custom tactics is crucial for …