Harold Williams, USC

Title: An Introduction to Automated Theorem Proving in Lean

Abstract: In this talk we will give an introduction to Lean, a programming language adapted to the formal verification of mathematical proofs. Lean and its flagship library, mathlib, have been the focus of a dedicated user community for about a decade, but their visibility has grown significantly in light of recent advances in AI.

Lean-based automated theorem provers are now improving at a steady pace, and we will compare and contrast the training of such systems with the training of large language models such as GPT, Claude, or Gemini. We will also give a brief introduction to Monte Carlo Tree Search, an algorithm whose presence or absence provides one of the main high-level distinctions among different state-of-the-art automated provers. Its use in particular distinguishes Seed-Prover and Aristotle, two frontier models developed respectively by ByteDance and Harmonic, the latter in collaboration with an academic team including myself, Sergei Gukov, Dan Halpern-Leistner, and Alex Meiburg.