Date: Thursday, November 6, 2025
Time: 11:45 a.m. to 12:45 p.m.
Location: G01 Gates Hall
Speaker: Leonardo de Moura, Senior Principal Applied Scientist, Automated Reasoning Group at AWS
Abstract: Imagine a world where mathematicians, programmers, and AI systems can collaborate with complete trust in each other's work. This is the promise of Lean, an open-source project that's transforming how we approach mathematics, software development, and artificial intelligence. Lean provides machine-checkable proofs, eliminating the need for manual verification and allowing humans and AI to build upon each other's work with confidence.
By addressing the "Trust Bottleneck," Lean opens doors to cross-disciplinary collaboration. In this talk, we'll explore how Lean is impacting these fields. We’ll see how it's providing mathematicians with a new way to construct and verify complex proofs, enabling software developers to rigorously verify critical systems, and creating a foundation for more reliable AI for science and mathematics. We'll also discuss the role of the Lean Focused Research Organization (FRO), a non-profit dedicated to advancing Lean and growing its community. The FRO is driving Lean's development as both a proof assistant and an extensible programming language, empowering users to customize its capabilities for diverse applications. Through real-world examples from academia and industry, we'll discover how Lean is paving the way for a more efficient, reliable, and collaborative future in mathematics, software development, and AI. 
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. Leo’s work has also been reported in the New York Times and many popular science magazines such as Wired, Quanta, Nature News, and Scientific American.
Website : https://leodemoura.github.io/about.html