1 h 25 min
Seminar, Hosted by Simons Institute for the Theory of Computing, UC Berkeley
Machine-Checked Proofs and the Rise of Formal Methods in Mathematics | Theoretically Speaking
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 assistant, search World Wide
- interactive mathematical proofs, search World Wide
- mechanically verified software, broader topic: software
- extensibility, search World Wide
- collaborative formalisation, search World Wide
- Liquid Tensor Experiment, search World Wide
- Mathematics Education
- AI-generated proofs