> ZFC was never intended as a language for practically doing mathematics in, so that's a weird criticism.
Isn't that just the point? Currently we do metamathematics in an esoteric language where your normal mathematical tools won't always have the meaning you expect them to have - HoTT is about enabling us to do it in something much closer to normal mathematics.
> Could you give an example of how definitions from, say, probability theory and algebraic geometry might be merged in a useful way?
A lot of category theory is "this theorem from this context can be translated to this theorem in this other context". Do I know any specific equivalences between probability distributions and multivariate polynomials? No. But I wouldn't be at all surprised if we found some. At one point the idea that arithmetic could tell us something about geometry was a surprising and novel one.
> I think this comment misunderstands the problem with the ABC "proof," which is (speaking roughly) that a certain lemma asserted something that was crucial to the argument, but which was never actually proved. Peter Scholze and others spotted this pretty quickly. Formalization wouldn't really have helped at all.
The fact that it was disputed for at least two years whether that lemma was or wasn't valid is the fact that formalisation would have been helpful.
Isn't that just the point? Currently we do metamathematics in an esoteric language where your normal mathematical tools won't always have the meaning you expect them to have - HoTT is about enabling us to do it in something much closer to normal mathematics.
> Could you give an example of how definitions from, say, probability theory and algebraic geometry might be merged in a useful way?
A lot of category theory is "this theorem from this context can be translated to this theorem in this other context". Do I know any specific equivalences between probability distributions and multivariate polynomials? No. But I wouldn't be at all surprised if we found some. At one point the idea that arithmetic could tell us something about geometry was a surprising and novel one.
> I think this comment misunderstands the problem with the ABC "proof," which is (speaking roughly) that a certain lemma asserted something that was crucial to the argument, but which was never actually proved. Peter Scholze and others spotted this pretty quickly. Formalization wouldn't really have helped at all.
The fact that it was disputed for at least two years whether that lemma was or wasn't valid is the fact that formalisation would have been helpful.