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 sheet of the first class, to get an impression.
Video recording Lean file used Slides
2. Logic: basic proofs using tactics intro, apply, exact, trivial, and exfalso.¶
In this class we started to prove basic (and trivial) statements in propositional logic. For reference about the tactics we were using, see notes by Bhavik Mehta.
The homework is in the repo (also linked in below -- as a file and as link to live server).
Submit the homework via postal owl, you should've gotten enroll link by email.
Video recording A Video recording B Class github repo Homework Homework on live-lean
3. Logic: more proofs using tactics cases, constructor, left/right, rw, rfl. Real numbers: ring, or norm_num. Also use.¶
We learned techniques to deal with conjuction (cases, constructor) and disjunction (left/right and cases again).
There are two tactics in each case, because assumptions and goal work differently.
We saw several ways to get shorter proofs: using assumption together with <;>, and a diabolical tactics rcases.
We also started a bit with real numbers -- so far just the easy way using tactics ring and norm_num that do the
trivial stuff for us.
We also saw intro to deal with "for all" quantifier and use for existential quantifier.
Video recording A Video recording B Video recording C Homework Homework on live-lean
4. Real numbers: dealing with sequences and quantifiers (intro, specialize, use, obtain). First glimpse of types.¶
We proved basic theorems about limits of sequnces of real numbers. Mainly as a motivation to learn new techniques:
- defining a lambda function (keyword fun)
- dealing with quantifiers: intro and specialize for \(\forall\), use and obtain for \(\exists\))
- linarith, norm_num and ring_nf for simplifying expressions with real numbers
- exact? for easy search for the right theorem in the mathlib
In the end we learned a bit about types; we will learn more next week.
Video recording A Video recording B Video recording C Homework Homework on live-lean