4 ms·

> How is this not partial evidence that ZFC is trash? ZFC was never intended as a language for practically doing mathematics in, so that's a weird criticism.

> How is this not partial evidence that ZFC is trash? ZFC was never intended as a language for practically doing mathematics in, so that's a weird criticism. > Mainstream mathematicians do run the risk of being siloed in narrow specialties because abstractions are needed to distill the all definitions of remote areas of mathematics. Mathematicians are siloed in narrow specialties because they focus on solving hard problems that require a great deal of specific subject matter expertise. I strongly doubt that "distill[ing] the all definitions of remote areas of mathematics" is even possible, or a fruitful project to attempt. Could you give an example of how definitions from, say, probability theory and algebraic geometry might be merged in a useful way? > No you need formal proofs to check that there aren't errors along the way. And lack of formal proofs slows down new weird stuff like the ABC conjecture proof candididate. 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.

lmm 6y ago
> 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.

lmm 6y ago

> 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.