Comment by Davidzheng
11 hours ago
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.
11 hours ago
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.
we are moving forward steadily :) https://github.com/marcinjangrzybowski/cubical-bis/blob/inte... (see table in the middle of doc) mind, that it is fully constructive implementation, you can get arbitrary precision aproximation to every real expression. for now WIP, but soon will be aviable in cubical-library :) also our related TYPES2026 presentation: https://types2026.cse.chalmers.se/slides/51.pdf
Last week I blew my whole Claude Max weekly budget having Opus translate from Mathlib to Coq-HoTT. It was so beautiful I can't wait to do it again this week.
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.
Why is that sad?
The stronger AI become the easier it should be to develop and move to alternative foundations.
Hey now... If you have a formulation in type theory (lean is not set theory), then you can translate to homotopy type theory fairly easily
[flagged]