Makes me sad that the homotopical foundation people never got their shit together and now formalization is so mature but it's still done in set theoretic foundations.
What you mean it say is that Lean is not a HoTT, and Mathlib has tons of classical reasoning (excluded middle, axiom of choice).
I don't think it's too late at all for HoTT. In fact, I think the AI companies will find trying to crank out more new math which is out of distribution in a funky way a highly useful exercise.
Lean's type theory kinda gives up on that idea: Mathlib gleefully postulates impredicative propositions with the axiom of choice, quotient types, etc. All in all, I'd say that Lean is much closer in spirit to De Bruijn's AUTOMATH project (which pre-dates Martin-Löf!), whose goal was to formalise classical math textbooks using dependent types.