Verified Collaboration: How Lean is Transforming Mathematics, Programming, and AI
- Speaker
-
Leonardo de Moura, Ph.D.Senior Principal Applied Scientist, Automated Reasoning Group, Amazon Web Services
Presidential Lectures are a series of free public colloquia spotlighting groundbreaking research across four themes: neuroscience and autism science, physics, biology, and mathematics and computer science. These curated, high-level scientific talks feature leading scientists and mathematicians and are designed to foster discussion and drive discovery within the New York City research community. We invite those interested in these topics to join us for this weekly lecture series.
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 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 on each other’s work with unprecedented confidence. By addressing the “trust bottleneck,” Lean opens doors to cross-disciplinary collaboration.
In this Presidential Lecture, Leonardo de Moura will provide an overview of Lean’s impact. He’ll show how Lean provides mathematicians a new way to construct and verify complex proofs, enables software developers to rigorously verify critical systems, and creates a foundation for more reliable AI for science and mathematics. Through real-world examples from academia and industry, he’ll present how Lean is paving the way for a more efficient, reliable and collaborative future.
About the Speaker
De Moura is a senior principal applied scientist in the Automated Reasoning Group at Amazon Web Services. In his spare time, he dedicates himself to serving as the chief architect and a board member of the Lean Focused Research Organization, a nonprofit organization he co-founded with Sebastian Ullrich. Before joining AWS in 2023, he was a senior principal researcher in the RiSE group at Microsoft Research and a computer scientist at SRI International. His research areas are automated reasoning, theorem proving, decision procedures, the boolean satisfiability problem and satisfiability modulo theories. He is the main architect of several automated reasoning tools: Lean, Z3, Yices 1.0 and SAL. His work in automated reasoning has been acknowledged with several prestigious awards, including the CAV Award, the Haifa Award, the Herbrand Award and the ACM’s Programming Languages Software Award.