3 ms·

> No one "does mathematics" in ZFC. How is this not partial evidence that ZFC is trash? > Mainstream mathematicians are not being prevented from proving theor

> No one "does mathematics" in ZFC. How is this not partial evidence that ZFC is trash? > Mainstream mathematicians are not being prevented from proving theorems because they lack "better ways of reasoning about equality of types." 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. Saying HoTT is a failure because people do informal proofs is rather moving the goal posts; people won't do formal proofs until the tooling is really good. But none of the up-and-comming tools are classic first order logic + ZFC (Please don't mention TLA+) and there's a reason for that. > The importance of ZFC is that it ensures our common language reasoning isn't incoherent (among other things). Once you've done that, you don't need to do it again. 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 don't expect this to be solved now (tooling, as per above), but mathematicians should learn more category theory now as that works just fine pencil paper and brain. When the type theoretic tooling is ready they will be ready.

spekcular 6y ago
> 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.
boyobo 6y ago
> No one "does mathematics" in ZFC. How is this not partial evidence that ZFC is trash? What percentage of coders do programming on a turing tape? Is this partial evidence that turing tapes are trash? Does that question even make sense? > I don't expect this to be solved now (tooling, as per above), but mathematicians should learn more category theory now as that works just fine pencil paper and brain. When the type theoretic tooling is ready they will be ready. The abstractions of category theory are useless in many areas of mathematics. Prime example: PDEs. Laypeople think that category theory is the 'ultimate math' because they hear that it provides bridges or analogies between different areas of math. Perhaps programmers are especially prone to this because category theory does have some applications to programming. The thing is, almost all of pure math is itself is a bridge between different areas of math. Some of these areas are bridged by category theory, some are bridged by other kinds of math, which have less catchy names.
- Ericson2314 6y ago
  > What percentage of coders do programming on a turing tape? Is this partial evidence that turing tapes are trash? Does that question even make sense? ZFC should be more like machine code we actually use than turn tape concept which we don't. The fact that no one uses something higher level that compiles down to ZFC is disheartening. As the FOM mailing list demonstrates, it's really about goal posts here. For one camp, the goal posts are such that ZFC or many other things are equally good. ZFC by share age has the "large cardinal" advantage in that people have been grinding away at it longer. For the other camp, large-cardinal-type research agendas aren't very interesting, and the goal posts are dramatically different. I still think ZFC is trash, but I will admit my mistake in thinking other share my goal posts. > The abstractions of category theory are useless in many areas of mathematics. For example, PDEs. At the moment that is true. But I think this is more due to the human concerns than the actually Math. Until Statistics overtook it, differential equalization were the most-applied branch of mathematics, which definitely influenced the culture around it. There is also the general algebraist---analyst cultural divergence. I look forward to the day when the computer tools are so good they are used in those fields too. That should bridge the culture gap, and then we shall see what the math holds.
- lmm 6y ago

spekcular 6y ago

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

boyobo 6y ago

> No one "does mathematics" in ZFC. How is this not partial evidence that ZFC is trash? What percentage of coders do programming on a turing tape? Is this partial evidence that turing tapes are trash? Does that question even make sense? > I don't expect this to be solved now (tooling, as per above), but mathematicians should learn more category theory now as that works just fine pencil paper and brain. When the type theoretic tooling is ready they will be ready. The abstractions of category theory are useless in many areas of mathematics. Prime example: PDEs. Laypeople think that category theory is the 'ultimate math' because they hear that it provides bridges or analogies between different areas of math. Perhaps programmers are especially prone to this because category theory does have some applications to programming. The thing is, almost all of pure math is itself is a bridge between different areas of math. Some of these areas are bridged by category theory, some are bridged by other kinds of math, which have less catchy names.

Ericson2314 6y ago
> What percentage of coders do programming on a turing tape? Is this partial evidence that turing tapes are trash? Does that question even make sense? ZFC should be more like machine code we actually use than turn tape concept which we don't. The fact that no one uses something higher level that compiles down to ZFC is disheartening. As the FOM mailing list demonstrates, it's really about goal posts here. For one camp, the goal posts are such that ZFC or many other things are equally good. ZFC by share age has the "large cardinal" advantage in that people have been grinding away at it longer. For the other camp, large-cardinal-type research agendas aren't very interesting, and the goal posts are dramatically different. I still think ZFC is trash, but I will admit my mistake in thinking other share my goal posts. > The abstractions of category theory are useless in many areas of mathematics. For example, PDEs. At the moment that is true. But I think this is more due to the human concerns than the actually Math. Until Statistics overtook it, differential equalization were the most-applied branch of mathematics, which definitely influenced the culture around it. There is also the general algebraist---analyst cultural divergence. I look forward to the day when the computer tools are so good they are used in those fields too. That should bridge the culture gap, and then we shall see what the math holds.
lmm 6y ago