The book presents Leo's vision for Lean and the development of Mathlib as two interdependent stories that are sometimes in tension.

“So what you need to do is equip it with a library of definitions. And this is at the parallel story in my book. There are kind of two key stories, two dreams almost, that are very dependent on each other, sometimes in tension with each other.”

“So one is Leo's vision for Lean, the software he wants to build. The other is the development of what comes to be called Mathlib, a library of digital mathematics, which is spearheaded by several of the main characters in the book.”