4 ms·

Yeah, they should have heard about ZFC and have a notion what a formal proof is. On the other hand, I'm not sure your last sentence is really that relevant. >

Yeah, they should have heard about ZFC and have a notion what a formal proof is. On the other hand, I'm not sure your last sentence is really that relevant. > They don't know anything about type theory, implications of the law of excluded middle, univalent foundations, any of that stuff I'm doing a PhD in algebraic geometry, and that stuff isn't relevant at all. To me "everything is a set" pretty much applies. Hell, even the stacks-project[1] contains that phrase! [1] https://stacks.math.columbia.edu/tag/0009 https://stacks.math.columbia.edu/tag/0009

JoeyBananas 2y ago
> I'm doing a PhD in algebraic geometry, and that stuff isn't relevant at all. Yes, exactly. These are topics that 99% of legit mathematicians don't know or care about. It's like saying "I'm a computer expert" when you only know Python, and then a computer engineer that designs CPUs starts laughing at you
- Tainnor 2y ago
  I don't understand the point of your comments.
  - JoeyBananas 2y ago
    My claim is that mathematics as practiced by mathematicians is not as rigorous as they think it is, and infact they're not even aware of the advances in rigorous mathematics that they're not using. Even though those advances are super important.
    - Tainnor 2y ago
      What important discoveries have you made using your supposedly "more rigorous" mathematics?
      - JoeyBananas 2y ago
        Loaded question
        Tainnor 2y ago
        Well, you've been claiming that these advances are "super important" and that set theory is not rigorous, but you have provided no evidence for either claim.
        JoeyBananas 2y ago
        I never said "set theory is not rigorous." Euclid wrote Elements without knowing anything about set theory. Math was done for thousands of years without modern set theory or any modern notion of logical foundations. Set theory is more rigorous than what came before it. It's not as rigorous as type theory (yes, this is an umbrella term) because type theory can be verified by a computer. Homotopy type theory is an example of the type of math that set theory can't handle There are so many layers of ignorance to unpack here and I don't care to be your unpaid tutor
        Tainnor 2y ago
        > because type theory can be verified by a computer proofs in FOL can be checked by a computer without any need for type theory - just look at metamath.

JoeyBananas 2y ago

> I'm doing a PhD in algebraic geometry, and that stuff isn't relevant at all. Yes, exactly. These are topics that 99% of legit mathematicians don't know or care about. It's like saying "I'm a computer expert" when you only know Python, and then a computer engineer that designs CPUs starts laughing at you

Tainnor 2y ago
I don't understand the point of your comments.
- JoeyBananas 2y ago
  My claim is that mathematics as practiced by mathematicians is not as rigorous as they think it is, and infact they're not even aware of the advances in rigorous mathematics that they're not using. Even though those advances are super important.
  - Tainnor 2y ago
    What important discoveries have you made using your supposedly "more rigorous" mathematics?
    - JoeyBananas 2y ago
      Loaded question
      - Tainnor 2y ago
        Well, you've been claiming that these advances are "super important" and that set theory is not rigorous, but you have provided no evidence for either claim.
        JoeyBananas 2y ago
        I never said "set theory is not rigorous." Euclid wrote Elements without knowing anything about set theory. Math was done for thousands of years without modern set theory or any modern notion of logical foundations. Set theory is more rigorous than what came before it. It's not as rigorous as type theory (yes, this is an umbrella term) because type theory can be verified by a computer. Homotopy type theory is an example of the type of math that set theory can't handle There are so many layers of ignorance to unpack here and I don't care to be your unpaid tutor
        Tainnor 2y ago
        > because type theory can be verified by a computer proofs in FOL can be checked by a computer without any need for type theory - just look at metamath.