Lectures¶
1. Introduction, motivation.¶
In the first class we looked at how does a formalized proof (proof verified by a computer) look like on somewhat advanced examples (Cantor theorem, squeeze theorem). The idea is not to understand everything, but to get impression, what this will be about: what is an ITP, how does this interactivity look like.
Homework (ungraded): install Lean and go through the files yourself.
2. Propositional logic.¶
Today, we started from the beginning: looking at how to deal with formulas, implications, conjuctions, etc. Way to submit homeworks will be specified soon. Deadline Oct 20 (but if you tried some parts before the 3rd class, it'd be good for you).