Learning Lean: Part 2

I am continuing to learn Lean (see part 1) by going through Mathematics in Lean. These are my notes as I just finished chapters one through five. Mathematics in Lean The online book is well-paced and well-written to connect with what an average student of mathematics already knows. The focus is on learning how to do basic mathematical proofs in Lean, and the underlying language is taught as needed for those goals, in comparison to Theorem Proving in Lean which is more of a language guide. For example, the fact that naturals are constructed as an inductive type with zero and succ constructors is shown much after one is shown how to work with them. This is aligned with how a lot of mathematics is done before one discusses foundations in a typical mathematics curriculum, which might differ from a CS one.

rkirov.github.io · Rado's Radical Reflections