week11--formalization.md

---

title: |
 Week11 -- Formalization of Math
author: George McNinch  
date: 2024-04-01

---

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)!