Search, Reason or Recombine? Paradigms for Scaling Formal Proving

This 54-minute lecture by Fabian Glöckle from Ecole Nationale des Ponts et Chaussées and FAIR at Meta explores the competing paradigms for scaling formal theorem proving with language models. Examine the contrast between large-scale search methods using reinforcement learning (like AlphaProof) and long chain-of-thought reasoning with emergent self-verification (as in o1). Discover the spectrum of hybrid approaches, including line-level tree search with environment feedback, multi-turn iterative whole proof generation, and hierarchical problem decompositions with partial proof recombination. Learn about these methods as inference techniques and understand the challenges of applying reinforcement learning to formal proving. The lecture is presented at the Institut des Hautes Etudes Scientifiques (IHES) and is available on CARMIN.tv, a French video platform specializing in mathematics and interdisciplinary scientific content.