1 h 25 min
Machine-Checked Proofs and the Rise of Formal Methods in Mathematics | Theoretically Speaking
Mathematics, Computer Science and Software Engineering seminar by Leonardo de Moura, AWS
Hosted by Simons Institute for the Theory of Computing, UC Berkeley
Thursday 17:30 Los Angeles (GMT-7)
Recording available
Berkeley, United States
Recording
Abstract
Leonardo de Moura explains how the Lean proof assistant supports interactive mathematical proofs and mechanically verified software. The lecture discusses extensibility, collaborative formalisation and Lean’s mathematical library, with examples from the Liquid Tensor Experiment, mathematics education and the verification challenges associated with AI-generated proofs.
Topics
Lean proof assistantinteractive mathematical proofsmechanically verified softwareextensibilitycollaborative formalisationLiquid Tensor ExperimentMathematics EducationAI-generated proofs
Related seminars
AI for Formal Math, and Physics, and why they're different
Video · 1 h 16 min · Apr 15, 2026Alexander Meiburg, Perimeter Institute for Theoretical PhysicsMathematics in the Age of AI: Discovery, Reasoning, Verification, and Unease
Oct 20, 2026Ken Ono, University of Virginia and Axiom MathAI is a tool: A working mathematician's experience and perspective
Nov 16, 2026Martin Raum, Chalmers University of Technology
More from Simons Institute for the Theory of Computing, UC Berkeley
All talksOptimal Spectral Gaps | Richard M. Karp Distinguished Lecture
Oct 14, 2026Ramon van HandelMy Favorite Expanders | Richard M. Karp Distinguished Lecture
Sep 29, 2026Ryan O'DonnellEncrypting to a Mathematical Fact | Theoretically Speaking
Video · 1 h 24 min · Captions · Jul 15, 2026Sanjam GargResponsibly Improving AI with Privacy-Sensitive Data: Principles, Theory, and Practice | Richard M. Karp Distinguished Lecture
Video · 1 h 10 min · Captions · Feb 24, 2026Brendan McMahan