> I've done some intro to lean things, but no one in the maths program is into lean, so I'm just focusing on the math side. Terry Tao is big into the idea of lean tho, and combining LLMs with Lean.

One of the best things about entering an underpopulated space is that you can become one of the leading experts very quickly. If it's something that appeals to you and fits your skill set, it might be worth investing the time to learn!

(Again, I say this as someone who's always been interested in formal proof, but haven't investigated it much myself, much less explored the merits and demerits of particular systems—so this is not an endorsement of Lean specifically, though it does seem to be one of the most active communities, which is important when you're trying to get into a topic.)