Formalizing the Future: Lean’s Impact on Mathematics, Programming, and AI
From Strachey Lectures by Oxford University
May 15, 2025 · 47 min
About this episode
Leo De Moura discusses the impact of the Lean proof assistant on mathematics, programming, and AI, emphasizing collaboration and formal verification.
Leo De Moura: Formalizing the Future: Lean’s Impact on Mathematics, Programming, and AI 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.
People in this episode
Host: Oxford University
Guest: Leo De Moura
Topics covered
- Lean proof assistant
- mathematics
- programming
- AI
- collaboration
- formal verification
Keywords
- Lean
- proof assistant
- mathematics
- software verification
- AI research
- collaboration
- formal reasoning
Mentioned in this episode
Organizations: Lean Focused Research Organization
More episodes of Strachey Lectures
- Hardening Digital Infrastructure: Two Examples · May 27, 2026 · 1h 2m
- An AI stack: from scaling AI workloads to evaluating LLMs · February 26, 2026 · 56 min
- Advances in Garbled Circuits · October 27, 2025 · 48 min
- Will Computers prove theorems? · May 15, 2025 · 46 min
- Privacy, Verification, Robustness: A Cryptographer's perspective on ML · March 11, 2025 · 1h 4m
- From probabilistic bisimulation to representation learning via metrics · December 2, 2024 · 55 min
Explore listener stats, chart rankings, contacts and more on the Strachey Lectures podcast page.