1. Top
  2. lean-iap
  3. Files
  4. index.html
lean-iap

IAP 2026 class about Lean (mirror)

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
  10. 10
  11. 11
  12. 12
  13. 13
  14. 14
  15. 15
  16. 16
  17. 17
  18. 18
  19. 19
  20. 20
  21. 21
  22. 22
  23. 23
  24. 24
  25. 25
  26. 26
  27. 27
  28. 28
  29. 29
  30. 30
  31. 31
  32. 32
  33. 33
  34. 34
  35. 35
  36. 36
  37. 37
  38. 38
  39. 39
  40. 40
  41. 41
  42. 42
  43. 43
  44. 44
  45. 45
  46. 46
  47. 47
  48. 48
  49. 49
  50. 50
  51. 51
  52. 52
  53. 53
  54. 54
  55. 55
  56. 56
  57. 57
  58. 58
  59. 59
  60. 60
  61. 61
  62. 62
  63. 63
  64. 64
  65. 65
  66. 66
  67. 67
  68. 68
  69. 69
  70. 70
  71. 71
  72. 72
  73. 73
  74. 74
  75. 75
  76. 76
  77. 77
  78. 78
  79. 79
  80. 80
  81. 81
  82. 82
  83. 83
  84. 84
  85. 85
  86. 86
  87. 87
  88. 88
  89. 89
  90. 90
  91. 91
  92. 92
  93. 93
  94. 94
  95. 95
  96. 96
  97. 97
  98. 98
  99. 99
  100. 100
  101. 101
  102. 102
  103. 103 
<!DOCTYPE html>
<html lang="en">

<head>
  <title>Programs and Proofs in Lean</title>
</head>

<body style="width:min(900px,90%);margin:auto">
  <h1 style="text-align:center">Programs and Proofs in Lean</h1>
  <p style="text-align:center"><a href="https://sipb.mit.edu/iap/2026/">SIPB IAP 2026</a></p>
  <p style="text-align:center">Taught by <a href="..">Anthony Wang</a></p>
  <hr>
  <h2>Description</h2>
  <p>
    Tired of debugging bad code? Interested in weird programming languages? Curious about using computers for doing math? In this fast-paced not-for-credit class, we'll learn the Lean programming language, which is probably radically different from any other language you've used before. We'll explore some of Lean's powerful features, such as dependent types, type classes, monads, local imperativity, and tactics. Hopefully, this class will give you a fresh new perspective on an alternative way of programming and doing math.
  </p>
  <p>
    <b>Prereqs:</b> 6.101 or equivalent, 6.120 or equivalent
  </p>
  <p>
    <b>Compared to 6.S057 Verified Software Engineering:</b> 6.S057 uses the Dafny automated theorem prover which has a long history of serious bugs. Don't use Dafny, it's unsound!
  </p>
  <p>
    <b>Compared to 6.512 Formal Reasoning About Programs:</b> 6.512 uses Rocq instead of Lean. I haven't actually taken it, but my friend said that class mostly just proves trivial things. This class will try to prove some nontrivial theorems too, using Lean's Mathlib library and modern automated tactics like <code>grind</code>.
  </p>
  <hr>
  <h2>Schedule</h2>
  <p><b>Location and time:</b> 6-7:30 PM, 3-370</p>
  <p><b>Office hours:</b> 3-5 PM, Jan {19, 22}, W20-557 (SIPB office)</p>
  <table>
    <tr>
      <th>Date</th>
      <th>Lecture</th>
      <th>Topics</th>
      <th>Recommended reading</th>
      <th>Pset</th>
    </tr>
    <tr>
      <td>Jan 16</td>
      <td><a href="slides.pdf">Why Lean?</a></td>
      <td>
        Cool Lean projects, history of proof assistants, ITPs vs ATPs, propositional logic, Curry-Howard, simply typed lambda calculus, first-order logic, dependent types, lambda cube, calculus of constructions
      </td>
      <td>TTbE (1-23)</td>
      <td><a href="Pset1.lean">Pset1.lean</a></td>
    </tr>
    <tr>
      <td>Jan 20</td>
      <td><a href="Basic.lean">Basic topics</a></td>
      <td>
        Basic syntax, induction (recursion), termination checking, inductive types, pattern matching, polymorphism, type classes, tactics for first-order logic, <code>grind</code>, Loogle
      </td>
      <td>TTbE (23-39), FPIL (Ch1-Ch3), TPIL (Ch1-Ch5)</td>
      <td><a href="Pset1.5.lean">Pset1.5.lean</a></td>
    </tr>
    <tr>
      <td>Jan 23</td>
      <td><a href="MoreBasic.lean">More basic topics</a></td>
      <td>
        Functors, applicatives, monads, <code>do</code> notation, IO, vectors, indexing proofs, <code>mvcgen</code>, Hoare triples
        <!-- Universes, <code>Prop</code> weirdness, choice, subtypes, quotients, algebraic hierarchies in Mathlib, denotational semantics -->
      </td>
      <td>FPIL (Ch4-Ch5), TPIL (Ch6-Ch12)</td>
      <td><a href="Pset2.lean">Pset2.lean</a></td>
    </tr>
  </table>
  <hr>
  <h2>Resources</h2>
  <ul>
    <li>
      <a href="https://forgejo.mit.edu/xy/lean-iap">Git repo for this class</a>
    </li>
    <li>
      <a href="https://cjquines.com/files/typetheory.pdf">Type Theory by Example</a> (made by another SIPB member!)
    </li>
    <li>
      <a href="https://slightknack.dev/blog/do-notation/">do notation</a> (written by my friend Isaac)
    </li>
    <li>
      <a href="https://leanprover-community.github.io/papers/lean-tactics.pdf">Tactics cheatsheet</a>
    </li>
    <li>
      <a href="https://loogle.lean-lang.org/">Loogle</a>
    </li>
    <li>
      <a href="https://lean-lang.org/learn/#core-documentation">FPIL, TPIL, MIL</a>
    </li>
    <li>
      <a href="https://github.com/lean-forward/logical_verification_2025">The Hitchhiker's Guide to Logical Verification</a>
    </li>
    <li>
      <a href="https://github.com/BartoszMilewski/DaoFP">The Dao of Functional Programming</a>
    </li>
    <li>
      <a href="https://leanprover-community.github.io/extras/pitfalls.html">Common Lean Pitfalls</a>
    </li>
    <li>
      <a href="https://leanprover-community.github.io/documentation.html">Lean docs overview</a>
    </li>
  </ul>
</body>

</html>