Seminar Details

In this talk, I’ll provide an overview of some advancements in AI and machine learning in proof assistant languages, such as Lean, Rocq, and Isabelle/HOL. I’ll discuss both neural and symbolic techniques for various proof assistant tasks, including automated proof synthesis, autoformalization, premise selection, and lemma conjecturing. With respect to neural techniques, I’ll cover the basics of applying language models, reinforcement learning, and graph neural networks to the theorem proving domain.