Lean: Machine-Checked Mathematics and Verified Programming, Past and Future
summary
Lean claims a small trusted core and full extensibility, with 2 million lines in Mathlib and 100,000 theorems verified; automation like grinds and a verified LRAT checker plus a BV decision tactic handle bitvectors and generate proofs; verified models (Cedar) run faster than Rust production and a Perfectoid-spaces formalization both fixes bugs and simplifies the original proof; tooling — Lake, VS Code integration, metaprogramming and parallel compilation — is production-ready and actively used in software and math projects.
AI-written summary · about
chapters (27)
- 0:00Introduction
- 1:24Lean’s origins and goals
- 3:55Lean for mathematicians
- 6:25Dependent type theory
- 11:47Proofs as terms
- 12:08Classical math support
- 14:14Mathlib impact
- 17:51Modern math formalization
- 21:25Liquid Tensor Experiment
- 24:18Quantum formalization
- 27:37Software verification
- 28:20Cedar at AWS
- 29:47Verified privacy
- 30:53Crypto at Microsoft
- 33:01Extensibility and DSLs
- 35:58Domain-specific languages
- 37:41Protocol verification
- 39:07Compiler verification
- 40:11Bit vector reasoning
- 44:07Lean hammers
- 47:02Proof automation diagnostics
- 48:49Grind reasoning tool
- 53:08Lean and AI
- 55:16AlphaProof
- 57:46Lean FRO mission
- 59:12CSLib future
- 1:02:06Q&A
related talks
22mA Certifying Proof Assistant for Synthetic Mathematics in Lean
19mVelvet: A Multi-Modal Verifier for Effectful Programs
15mA benchmark for vericoding: formally verified program synthesis
22mTowards Automated Verification of LLM-Synthesized C Programs
01h 16mCoding Agents: New opportunities for formal methods?
33mCorrectness Too Cheap To Meter: Formal Verification and LLMs
38mAutomatically Synthesising Programs that We Can Trust
01h 00mAI Safety through Programming?