leannotes

 Lean Lecture, Incomplete Notes

David Gross

These notes use the verso system, with adaptions by Davood Tehrani. We are grateful to the University of Cologne's Quantum Matter and Information Key Profile Area for support.

Contents

  1. 1. Introduction
  2. 2. Background: Intuitionist Logic, Constructive Mathematics, Type Theory
  3. 3. Some Computability Theory
  4. 4. From Nil to Nat: Arithmetic
  5. 5. From Nil to Nat: Logic