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

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.

You can listen to Formalizing the Future: Lean’s Impact on Mathematics, Programming, and AI online on Radio and Podcast. Open the player on this page to stream the available audio.

Formalizing the Future: Lean’s Impact on Mathematics, Programming, and AI is an episode from Computer Science by Oxford University.

This episode is 47:14 long.

This episode was published on May 15, 2025.

Yes. Use the heart button on the episode page to add it to your favorite episodes list.

Yes. This page shows related episodes from Computer Science when more episodes are available from the podcast feed.