Mathematics in the Age of AI
Lean: Machine-Checked Mathematics, Software, and AI
Speaker: Leonardo De Moura, AWS Automated Reasoning Group
Location: Warren Weaver Hall 109
Date: Saturday, November 14, 2026, 1:30 p.m.
Synopsis:
Lean is an open-source programming language and proof assistant. You can use it to write mathematical definitions, theorems, and proofs, and to write programs and prove that they are correct. A small kernel checks every proof. If the kernel accepts a proof, it does not matter whether a person or an AI wrote it.
Lean proofs are growing exponentially: in the last twelve months, they grew by three orders of magnitude. AI systems are auto-formalizing mathematics at large scale, translating published results into Lean, and proving open conjectures. New software and hardware verification projects have started. AI agents now write much of this code and many of these proofs.
In this talk, I will explain what Lean is and how it works, using simple examples. No background in Lean or formal methods is needed. I will then show how Lean is used in mathematics, software and hardware verification, and AI, and discuss the challenges ahead.
Notes:
Leo is a Senior Principal Applied Scientist in the Automated Reasoning Group at AWS. In his spare time, he dedicates himself to serving as the Chief Architect of the Lean FRO, a non-profit organization that he proudly co-founded alongside Sebastian Ullrich. He is also honored to hold a position on the Board of Directors at the Lean FRO, where he actively contributes to its growth and development. Before joining AWS in 2023, he was a Senior Principal Researcher in the RiSE group at Microsoft Research, where he worked for 17 years starting in 2006. Prior to that, he worked as a Computer Scientist at SRI International. His research areas are automated reasoning, theorem proving, decision procedures, SAT and SMT. He is the main architect of several automated reasoning tools: Lean, Z3, Yices 1.0 and SAL. Leo’s work in automated reasoning has been acknowledged with a series of prestigious awards, including the CAV, Haifa, and Herbrand awards, as well as the Programming Languages Software Award by the ACM. Leo’s work has also been reported in the New York Times and many popular science magazines such as Wired, Quanta, and Nature News.