I'm super excited about this. Hope it gets moved to its own repo so it's easier to find and send to other people. I was always curious about math, and Tao's Analysis was the first textbook that really showed me how it can be constructed in a rigoruous way my programming brain was hoping for. Then I got a bit into Lean, and similarly it was very satisfying but Mathlib is a bit complicated to learn math concepts from. So it's nice to see a bridge from the book to the tool.