Lean at MC 2022

• Introduction

• 1. Logic in Lean - Part 1
  • 1.1. Propositions as types
  • 1.2. Implications in Lean
  • 1.3. And / Or
  • 1.4. Negation
  • 1.5. Final Remarks
• 2. Logic in Lean - Part 2
  • 2.1. Behind the scenes
  • 2.2. The Law of the Excluded Middle
  • 2.3. Quantifiers
  • 2.4. Equality
• 3. Infinitely Many Primes
  • 3.1. Divisibility and Primes
  • 3.2. Trivial calculations
  • 3.3. Creating subgoals
  • 3.4. Infinitely many primes
  • 3.5. Final remarks
• 4. Sqrt 2 is irrational
  • 4.1. Implicit arguments
  • 4.2. The two haves
  • 4.3. Sqrt(2) is irrational
• 5. Bits & Pieces
  • 5.1. Namespaces
  • 5.2. Coercions
  • 5.3. Type classes
  • 5.4. Recursion and Induction

• Pretty Symbols in Lean
• Glossary of Tactics and Lemmas