Physical books about Lean and/or Mathlib?

Stream: new members

[Isak Colboubrani]

I’m aware of several excellent online books for Lean and Mathlib (such as MIL, TPIL, HGLV, FPIL, MOP, etc.).

However, I’m wondering whether there are any physical books (i.e., with an ISBN and available for purchase from retailers like Amazon) about Lean and/or Mathlib beyond the following:

• "Exploring Formalisation: A Primer in Human-Readable Mathematics in Lean 3 with Examples from Simplicial Topology" (2022) by @Clara Löh
• "Maths Proofs in Lean: First Steps" (2025) by @rzeta0 (GitHub repo)
• The upcoming "The Proof in the Code" (2026) by @Kevin Hartnett

Is this list complete, or are there other ISBN-registered books currently available—or soon to be published—that I might be missing?

[Luigi Massacci]

The last one is supposed to be a pop-sci book, it's a bit weird to put it next to the others

[Luigi Massacci]

Also, while it's not about lean specifically (much too old), The Handbook of Practical Logic and Automated Reasoning is a great classic for the computer science side of things, and it's definitely available in print

[Kevin Buzzard]

Heather's book will, I believe, become a physical book one day.

[Isak Colboubrani]

The last one is supposed to be a pop-sci book, it's a bit weird to put it next to the others

@Luigi Massacci 2 is the only even prime number. Would you find it to be “weird” to include it with the others if someone asked for a list of all primes under, say, 10?

[Kevin Buzzard]

It is weird to claim that it is an "excellent online book for Lean and mathlib" given that it will contain absolutely no information about how to use Lean or mathlib, and no code at all, and is instead a historical discussion about the growth of the community suitable for a general audience, in stark contrast to the other references.

[Isak Colboubrani]

@Kevin Buzzard Who claimed that? :)

[Isak Colboubrani]

"Physical books about Lean and/or Mathlib?"

"I’m wondering whether there are any physical books about Lean and/or Mathlib beyond the following:"

[Kevin Buzzard]

Indeed it is about Lean and mathlib :-)

[Isak Colboubrani]

Yes, that’s precisely my point :)

[Isak Colboubrani]

@Kevin Buzzard Thanks! Adding "The Mechanics of Proof" by @Heather Macbeth to the list of (possible) future publications. I'll buy a copy as soon as it is available!

[Luigi Massacci]

Isak Colboubrani said:

Luigi Massacci 2 is the only even prime number. Would you find it to be “weird” to include it with the others if someone asked for a list of all primes under, say, 10?

Well, it is indeed quite common for theorems in arithmetic to start by "let $p$ be a prime number other than two..."
I didn't in any case mean it as some kind of aggressive critique, I just meant to underline the point. The following is also a list of physical books "about space" ; -)

• O'Neill, Barrett. Semi-Riemannian Geometry with Applications to Relativity. San Diego New York Berkeley, etc.: Academic Press, Inc. , C 1983, 1983. Print. Pure and Applied Mathematics 103.

• Galileo Galilei. Systema Cosmicum. Elsevier, 1635. isbn: 978-1-4933-0405-9.
  doi: doi.org/10.1016/B978-1-4933-0405-9.50007-2

• Adams, Douglas. The Hitchhiker's Guide to the Galaxy. New York: New York : Del Rey , 2005, 2005. Print. The Hitchhiker's Guide to the Galaxy 1.

[Isak Colboubrani]

That would have been a great analogy if the set of books “about space” had cardinality three ;)

Now, let’s make this thread more helpful for posterity by focusing on the original question at hand.

[Tyler Josephson ⚛️]

“The Big Bang of Numbers” (ISBN 1324065931) is a pop sci book that’s kind of like the Natural Number Game, but it’s more about the idea of informally deriving all math from basic axioms than it is about doing that with a proof assistant. Author is a colleague of mine at UMBC.