4. A first encounter with Lean 4#
There is no better way to learn how to formalize mathematics than to jump head-first into it. At first using a proof assistant may feel complicated and a bit overwhelming. Luckily, Lean 4 has very good learning resources that we shall rely on.
In class we will look at GlimpseOfLean by Patrick Massot, an introduction that takes about 2 to 3 hours to complete. A more thorough and slow-paced learning resource is Mathematics in Lean by the same author.
4.1. Homework#
There is a saying in Slovene, “Vaja dela mojstra” (exercise makes a master), with the side-condition “če mojster dela vajo” (if the master does exercises). It applies perfectly to learning formalized mathematics – there is no other way but to do it. Thus, your task for the week is as follows:
Complete the exercises in
GlimpseOfLean, and at least one extra topic.Read a good chunk of Mathematics in Lean. It is highly recommended that you familiarize yourself with chapters 1, 2, 3 and 4.