Lean4Lean - Formalizing the Type Theory of Lean

Explore a comprehensive lecture on formalizing the type theory of Lean, presented by Mario Carneiro at the Hausdorff Center for Mathematics. Delve into the intricacies of Lean4Lean, a project aimed at creating a formal specification of Lean's type theory within Lean itself. Gain insights into the challenges and methodologies involved in this meta-theoretical endeavor, which seeks to enhance the reliability and consistency of the Lean proof assistant. Learn about the techniques used to represent Lean's complex type system, including dependent types, universes, and inductive types, within its own framework. Discover how this formalization effort contributes to the broader field of proof assistants and formal verification, potentially leading to more robust and trustworthy mathematical proofs and software systems.

Mario Carneiro: Lean4Lean: Formalizing the type theory of Lean