Theorem Proving in Lean 4

 Theorem Proving in Lean 4

Jeremy AvigadLeonardo de MouraSoonho KongSebastian Ullrich

with contributions from the Lean Community

This version of the text assumes you’re using Lean 4 (specifically v4.23.0). See the Quickstart section of the Lean documentation to install Lean. The first version of this book was written for Lean 2, and the Lean 3 version is available here.

Contents

  1. 1. Introduction
  2. 2. Dependent Type Theory
  3. 3. Propositions and Proofs
  4. 4. Quantifiers and Equality
  5. 5. Tactics
  6. 6. Interacting with Lean
  7. 7. Inductive Types
  8. 8. Induction and Recursion
  9. 9. Structures and Records
  10. 10. Type Classes
  11. 11. The Conversion Tactic Mode
  12. 12. Axioms and Computation