Okay, yeah my response is ultimately based on the one conversation about it that I've had with the one prof of the one math class I've taken in the last 30 years, so take that with a grain of salt.

(Tangentially, I'm so so so so angry that universities stopped offering remote classes after covid. I'd been wanting to take a bunch of classes for a long time, but it's just not feasible when you've got a full-time job in the 'burbs. I managed to get through measure theory and quantum mechanics while the window was open, and it was great. I planned to get through a few more in differential geometry and algebraic topology, but then the window closed. Feels like I'll pretty much have to wait until retirement at this point. Oh well, first-world problems.)

Edit: oh and actually, follow-up question: are these tools useful for _learning_ advanced mathematics? I looked up in Lean and its approach to topology is very non-standard, which makes me question whether I'd actually be learning math or whether I'd mainly be learning how to finagle things into Lean-friendly representations but missing the higher-level concepts.