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 Ana

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.