Presenter: Linyu Yang
Abstract: This talk presents recent progress in integrating classical techniques with large language models for lemma synthesis in interactive theorem proving, particularly in the context of equivalence proofs for functional programs. On the classical side, we primarily rely on the exhaustive proof search tool Canonical, together with traditional SMT solvers, to ensure the soundness of proof checking. However, these techniques are limited in forward reasoning, especially in generating and applying useful lemmas. To address this limitation, we leverage large language models for heuristic lemma generation. Finally, we outline the remaining challenges and discuss several possible directions for addressing them.
URL: