Week11 -- Formalization of Math

This week I plan to show you how to use Lean to prove basic assertions in propositional logic. Along the way we’ll learn a variety of tactics.

I hope to have you work on problems during the lecture. I’ll show some examples, have you work for a bit (hopefully giving some feedback) and then I’ll show some more examples.

• lean code this week

  • [02–some-tactics-and-logic (via gitpod)]
    [github – 02–some-tactics-and-logic.lean]
  • [03–more-logic (via gitpod)]
    [github – 03–more-logic.lean]

There are exercises in those files (that is what I hope we’ll work on during the lecture); I’ve put solutions to them in the sub-directory:

• [github – solutions]

But you should try the problems before peeking at solution(s)!