## 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. ;)

#### Miguel Raz Guzmán Macedo (Apr 03 2020 at 13:38):

Jasmin this is awesome! Congrats on the new book version!

#### Patrick Massot (Apr 03 2020 at 14:54):

By the way, I went to the Lean forward web page and noticed Anne's paper. Was is mentioned here? I opened a PR to the paper list.

Merged.

#### Alistair Tucker (Apr 12 2020 at 14:41):

I don't think the definition of fact (page 54) can be right.

rofl

#### Kevin Buzzard (Apr 12 2020 at 15:00):

@Jasmin Blanchette @Alexander Bentkamp @Anne Baanen you have a howler on p54 -- 0!=1

#### Alexander Bentkamp (Apr 12 2020 at 15:05):

Read the last paragraph of that section :grinning:

rofl

oops

#### Jasmin Blanchette (Apr 12 2020 at 19:27):

Oops indeed. "Return" should have been "returns".

#### Jasmin Blanchette (Apr 12 2020 at 19:28):

Page ix:

An important characteristic of this guide, which it shares with Knuth’s TeXbook [15], is that it does not always tell the truth.

#### Kenny Lau (Apr 12 2020 at 19:32):

wow, you have Hoare triples!

#### Jasmin Blanchette (Apr 12 2020 at 19:42):

Yeah, we're computer scientists (more or less). ;)

#### Alistair Tucker (Apr 12 2020 at 19:49):

(deleted)

Last updated: May 11 2021 at 23:11 UTC