Schedule

Videos of Fall 2025 Lean Lectures With the permissions of the speakers, the videos are posted here.

October 1, 2025 at 8 am U.S. Pacific Time (California) Speaker: Professor Kevin Buzzard, Imperial College London.
Title: "What is formalization and why does it matter?"
Video of talk Kevin has received the Whitehead Prize (2002) and Senior Berwick Prize (2008). Wikipedia page for Kevin , Kevin's 2022 ICM talk on YouTube

October 7, 2025 at 5 pm U.S. Pacific Time (California) Speaker: Professor Zaiwen Wen, Peking University.
Title: "Advancing Mathematical Formalization: Tools and Techniques for Lean".
Abstract:" This talk explores cutting-edge tools and methodologies designed to advance mathematical formalization in Lean. We begin by showcasing ReasLab, an online collaborative IDE (prove.reaslab.io), and optlib, a Lean library dedicated to mathematical optimization (github.com/optsuite/optlib), alongside our ambitious project to formalize key textbooks in optimization, convex analysis, numerical linear algebra and related fields. We then present three methodological advances: (1) tree-based premise selection, which leverages Lean's core representation to automate proof premise discovery; (2) a method for translating informal proofs into formal ones through a structured chain of states; and (3) structure-to-Instance theorem autoformalization (SITA), an approach to bridging abstract mathematical theories with their concrete applications. Collectively, our work aims to accelerate formalization workflows and enhance the accessibility of rigorous mathematical proof.

October 20, 2025 at 8 am U.S. Pacific Time (California) Speaker: Professor Alex Kontorovich, Rutgers University.
Title: "An Introduction to Lean + AI for Research Mathematicians."
Abstract: We'll do a "show and tell" of what it's like to try to formalize some basic mathematics in Lean, with help from AI.

October 27, 2025 at 8 am U.S. Pacific Time (California) Speaker: Professor Michael R. Douglas, Harvard CMSA. Title: "Formalizing the Axioms of Quantum Field Theory"

November 6, 2025 at 8 am U.S. Pacific Time (California) Speaker: Professor Patrick Massot, Laboratoire de Mathématiques d'Orsay in Université Paris-Saclay. Title: "Differential topology and geometry in Lean"

November 12, 2025 at 8 am U.S. Pacific Time (California) Speaker: Professor Sébastien Gouëzel, Université de Rennes 1 / CNRS. Title: "Classes of smooth functions in mathlib" Abstract: The goal of this talk is to illustrate how finding the right definition in proof assistants can be tricky, even for mathematical objects that are quite basic. We will focus on defining the class of C^n functions, showing why several natural definitions are not suitable. Along the way, we will discuss several not so-well known mathematical facts or counterexamples, justifying why the definition used in mathlib does not look like the usual one.

November 25, 2025 at 9:15 am U.S. Pacific Time (California) Note new time. Speaker: Professor Michael Rothgang (Universität Bonn). Title: "Differential geometry in mathlib: present and future" Slides
Abstract: Finding the right definitions in mathematics is hard work. Is is true on paper, and even more salient for working with proof assistants. A lot of mathematical thought went into the right definition for mathlib's manifold library: I will explain the key considerations, motivating why its definitions look as they do. Along the way, I will give an overview on differential geometry in mathlib. We will see what is currently in the library, what is coming soon and where you can help. I will also comment on the technical challenges of working with manifolds in Lean and how to address them. Time permitting, I will illustrate these points with two case studies, about submanifolds and bordism theory.