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

Lean at MC 2022

  • Introduction
  • 1. Logic in Lean - Part 1
  • 2. Logic in Lean - Part 2
  • 3. Infinitely Many Primes
  • 4. Sqrt 2 is irrational
  • 5. Bits & Pieces
  • Pretty Symbols in Lean
  • Glossary of Tactics and Lemmas

  • PDF version
  • Lean Live Editor
  • Lean Documentation
  • Leanprover Community

Quick search

©2022, Aaron Anderson, Apurva Nakade, Jalex Stark. | Powered by Sphinx 5.0.1 & Alabaster 0.7.12 | Page source