The Lean Theorem Prover

Explore the Lean theorem prover in this comprehensive lecture by Leonardo de Moura at the Paul G. Allen School. Delve into the goals, architecture, and key features of this open-source project developed by Microsoft Research and Carnegie Mellon University. Learn how Lean bridges the gap between interactive and automated theorem proving, offering a framework for user interaction and axiomatic proof construction. Discover its applications in formalizing datatypes, algebraic structures, homotopy type theory, category theory, and analysis. Gain insights into Lean's trusted kernel based on dependent type theory, integrated development environments, and rich API. Understand the project's long-term vision and its current capabilities in the field of automated reasoning and theorem proving.

Intro
THE LEAN THEOREM PROVER TEAM
INTRODUCTION: LEAN
SECONDARY GOALS
SOFTWARE VERIFICATION AND FORMALIZED MATHEMATICS
ARCHITECTURE
KERNEL
TWO OFFICIAL LIBRARIES
AGNOSTIC MATHEMATICS
FREEDOM TO TRUST
EXPORTING LIBRARIES
RECURSIVE EQUATIONS
TACTICS
STRUCTURES (ADDITIONAL INSTANCES)
STRUCTURES (CONCRETE INSTANCES)
SYLOW THEOREM
AUTOMATION IN LEAN
AUTOMATION (MAIN CHALLENGES)
CASTS
CONGRUENCE FOR HETEROGENEOUS EQUALITY
EXAMPLE
CONGRUENCE CLOSURE AND PROOF RELEVANCE