Zulip Chat Archive

Stream: new members

Topic: New version of *Logical Verification in Lean* book


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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. ;)

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 03 2020 at 13:38):

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

view this post on Zulip Patrick Massot (Apr 03 2020 at 14:53):

Shouldn't we put a link somewhere in https://leanprover-community.github.io/links/?

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Apr 03 2020 at 15:05):

Merged.

view this post on Zulip Alistair Tucker (Apr 12 2020 at 14:41):

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

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 15:00):

rofl

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 15:00):

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

view this post on Zulip Alexander Bentkamp (Apr 12 2020 at 15:05):

Read the last paragraph of that section :grinning:

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 15:06):

rofl

view this post on Zulip Alistair Tucker (Apr 12 2020 at 15:10):

oops

view this post on Zulip Jasmin Blanchette (Apr 12 2020 at 19:27):

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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 12 2020 at 19:32):

wow, you have Hoare triples!

view this post on Zulip Jasmin Blanchette (Apr 12 2020 at 19:42):

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

view this post on Zulip Alistair Tucker (Apr 12 2020 at 19:49):

(deleted)


Last updated: May 11 2021 at 23:11 UTC