@quantabooks.org just released their first book, on the story of Lean by @kevinhartnett.bsky.social. It's a great story, about a pretty significant part of what's happening in math right now.
www.quantabooks.org/books/the-pr...
The inside story of Lean, a computer program that answers the age-old question: How do you know if something is true?