Lean 4 books with direct PDF access

Stream: new members

[Isak Colboubrani]

I am compiling a list of Lean 4 (and/or Mathlib) books, prioritizing those available in PDF format that can be directly downloaded. This approach is primarily to facilitate students' access, ensuring they do not need to run commands to convert files into PDFs themselves.

Additionally, as a secondary focus, each book's PDF should have an official URL for the current version, to minimize the risk of link rot and ensure long-term availability.

The initial list was sourced from the "Learning Lean 4" page, emphasizing books with available official PDF versions. I have expanded this list with other relevant books found during my research.

Below is the current list of Lean 4 books in English, each with an easily accessible, official PDF of the current version:

• [Added!] Formalising Mathematics (Kevin Buzzard): https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2024/formalisingmathematics.pdf
• How To Prove It With Lean (Daniel J. Velleman): https://djvelleman.github.io/HTPIwL/How-To-Prove-It-With-Lean.pdf
• Logic and Mechanized Reasoning (Jeremy Avigad, Marijn J. H. Heule, Wojciech Nawrocki): https://avigad.github.io/lamr/logic_and_mechanized_reasoning.pdf
• Mathematics in Lean (Jeremy Avigad, Patrick Massot): https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf
• Metaprogramming in Lean 4 (Arthur Paulino, Damiano Testa, Edward Ayers, Evgenia Karunus, Henrik Böving, Jannis Limperg, Siddhartha Gadgil, Siddharth Bhat): https://github.com/leanprover-community/lean4-metaprogramming-book/releases/download/latest/Metaprogramming.in.Lean.4.pdf
• The Hitchhiker’s Guide to Logical Verification (Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, Jannis Limperg): https://github.com/blanchette/logical_verification_2023/raw/main/hitchhikers_guide.pdf

If you are aware of any other books meeting these criteria (Lean 4 and direct access to an official PDF), please let me know.

[Kevin Buzzard]

My course notes are kind of "work in progress" but satisfy your criteria: there's a pdf link at the bottom of https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2024/

[Kevin Buzzard]

Although if you are using a computer to read lean documentation then I would argue that pdf is not a good medium compared to the more interactive options available.

[Isak Colboubrani]

@Kevin Buzzard Thank you for the notification about the availability of your book in PDF format. I had overlooked this and have now included it in the updated list. (I really like your book!)

Regarding the preference of HTML versus PDF mediums: My usage varies depending on the context. I utilize HTML for expedient reference lookups and PDFs for their reliable search capabilities and offline accessibility. It is my hope that the remaining HTML-exclusive Lean texts (namely, "The Mechanics of Proof," "Theorem Proving in Lean 4," "The Lean 4 Manual," "Functional Programming in Lean," and "Type Checking in Lean 4") will also be made available in PDF format in the future.

[Eric Wieser]

I wouldn't remotely agree with PDFs having "reliable search"

[Eric Wieser]

(as I understand it, PDFs just store a list of letters and coordinates, and the viewer has to make some guess as to what the text really is and where the spaces go)

[Isak Colboubrani]

True, PDF text storage is basic, but single-word search in well-formed PDFs like textbooks is usually reliable for simple queries.