Lean: Machine-Checked Mathematics and AI Collaboration
Leonardo de Moura (Creator of Lean FRO)
Colloquium
Friday, May 8, 2026, 3:30 pm
ECE 105
Abstract
Lean is a proof assistant and programming language designed to make formal verification practical. In this talk, Leo will describe how Lean works, what it can do today, and where it is going. The core idea is simple: every mathematical claim and every program can be checked by a machine. This changes what collaboration looks like — between mathematicians, between engineers, and increasingly between humans and AI systems. The talk will cover recent work on proof automation and AI-assisted formalization, including experiments where multi-agent AI systems work autonomously on Lean tasks, as well as the Lean FRO, a nonprofit building Lean as long-term open infrastructure for mathematics and verified software.
BIO
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 ACM SIGPLAN Programming Languages Software Award twice for Z3 and Lean.
The University of Washington is committed to providing access, equal opportunity and reasonable accommodation in its services, programs, activities, education and employment for individuals with disabilities. Live captioning will be provided for this event. To request disability accommodation such as ASL interpretation, contact the Disability Services Office at least ten days in advance of the event at: (206) 543-6450/V, (206) 543-6452/TTY, (206) 685-7264 (FAX), or email at dso@u.washington.edu.