The Proof in the Code, Kevin Hartnett's new book on the development of Lean and Mathlib, is out today.
www.quantabooks.org/books/the-pr...
To mark the launch, two online panels with the author on June 11 and 12, both 5pm UTC. Registration in the reply.