Introduction to mathematical logic with Lean 4?

Stream: Lean for teaching

[Kevin Cheung]

Does anyone have experience teaching an introductory one-semester mathematical logic course with Lean 4 covering symbolic logic, propositional and predicate calculi, set theory and model theory? Logic and Proof seems to cover most of these topics. I wonder if there are there other additional resources that I'm not aware of. Pointers and insights appreciated.

[Dan Velleman]

This probably isn't really what you're looking for, but there are a couple of resources for using Lean to teach students to write proofs: my How To Prove It With Lean and Heather Macbeth's The Mechanics of Proof. Both contain a little bit of symbolic logic and set theory.

[Heather Macbeth]

There's also the book Logic and Mechanized Reasoning, by Jeremy Avigad, Marijn Heule, and Wojciech Nawrocki. This book is aimed at advanced undergraduates (whereas Dan's and my books target early undergraduate students), and it covers both propositional logic and first-order logic in some detail.

[Kevin Cheung]

Thanks for the suggestions. I'll look into those.