That's because it's the one I know and am using. I agree the devs are focusing on classical mathematics, but given Lean's dual purpose as a general-purpose pro

That's because it's the one I know and am using. I agree the devs are focusing on classical mathematics, but given Lean's dual purpose as a general-purpose programming language, one can imagine a workflow of writing Lean code and verifying it in the language. It's up to the community if they want to do this.