Comment by Ericson2314

No Type Theory won: Per Martin-Löf is still alive and should be able to confirm his work lives in some form in Lean. Zermelo and Fraenkel would be utterly confused, however.

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.