Lean4Lean: Mechanizing the Metatheory of Lean
summary
A complete reimplementation of the kernel is written in Lean and produces an executable Lean-written typechecker that is the first alternative to the C++ reference; it runs 20–50% slower but is fast enough to verify Mathlib. Large parts of the core infer/check/defeq algorithms are mechanically verified, invariants for caching are proved, and a critical soundness bug found (metadata overflow triggering panic) is fixed; undecidability of conversion and the unique-typing proof remain open, and a domain-theory route is being explored.
AI-written summary · about
chapters (15)
- 0:00Lean4Lean project intro
- 1:08Lean's type theory changes
- 3:21Lean4Lean kernel goals
- 6:29Lean4Lean kernel design
- 10:41Type theory foundations
- 16:26Undecidability in Lean
- 23:13Consistency proof
- 23:55Unique typing theorem
- 33:54Circular proof and relations
- 38:15Domain-theoretic soundness
- 41:10Verifying kernel impl
- 47:30Soundness bugs found
- 53:33Future work and algorithm
- 54:56Practical use and questions
- 55:18Q&A on native decide
related talks
22mThe Lean Mathematical Library
01h 01mMulti-Modal Verification of Distributed Systems in Lean
30mTrustworthy Formal Natural Language Specifications
19mLean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean
29mExplicit Refinement Types
19mVelvet: A Multi-Modal Verifier for Effectful Programs
19mPanel: Compilation Frameworks
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs