Zulip Chat Archive

Stream: new members

Topic: New version of Logical Verification in Lean book

Jasmin Blanchette (Apr 03 2020 at 12:36):

There aren't that many Lean tutorials around. One of them, formerly called Logical Verification in Lean, has now been thoroughly overhauled and given a new title (The Hitchhiker's Guide to Logical Verification):

https://github.com/blanchette/logical_verification_2020/raw/master/hitchhikers_guide.pdf
https://github.com/blanchette/logical_verification_2020

The book is intended primarily as an introduction to interactive theorem proving for MSc-level C.S. students (for a course at VU Amsterdam), but I'm told some mathematicans have succeeded at using it as a Lean tutorial. Mathematicians might want to spend less time on Chapter 5 ("Inductive Predicates") and skip all of Part III ("Program Semantics").

Any feedback welcome.

Kevin Buzzard (Apr 03 2020 at 13:21):

It's great that you have something on the real numbers! TPIL only ever dealt with core Lean and never mentioned any of the richer mathematical objects. I see that seeing basic, well-documented explanations of developments of simple mathematical theories is absolutely crucial for mathematicians who are learning. A mathematician beginner can't read mathlib's construction of the reals at all.

Jasmin Blanchette (Apr 03 2020 at 13:31):

The C.S. students usually complain about too much focus on math (Chapters 11-13, but also the guest lecture by Rob L. about p-adic numbers in lecture 14). Our students unfortunately know very little math, even by C.S. standard. Many have never heard about "groups". But hey, you got to teach them what they need, not what they want. ;)