Strachey Lecture: Formalizing the Future: Lean’s Impact on Mathematics, Programming, and AI

Strachey Lecture: Formalizing the Future: Lean’s Impact on Mathematics, Programming, and AI Originally uploaded on the University of Oxford Podcast page 15/05/2025 Abstract of Leo De Moura's Talk: How can mathematicians, software developers, and AI systems work together with complete confidence in each other’s contributions? The open-source Lean proof assistant and programming language provides an answer, offering a rigorous framework where proofs and programs are machine-checkable, shared, and extended by a broad community of collaborators. By removing the traditional reliance on trust-based verification and manual oversight, Lean not only accelerates research and development but also redefines how we collaborate. In this talk, I will highlight how Lean is being used to tackle challenging problems in mathematics, software verification, and AI research that depends on formally sound reasoning. I will also introduce the Lean Focused Research Organization (FRO), a non-profit dedicated to expanding Lean’s capabilities and community. By showcasing real-world examples, ranging from advanced research projects to industry-driven applications, I illustrate how Lean empowers us to innovate in a more reliable, transparent, and truly collective manner. The Strachey Lectures are generously supported by OxFORD Asset Management.