5 ms·

> ZFC hasn't been "replaced" by anything. My experience is the opposite: ZFC hasn’t been “replaced” in the sense that it never was - we always used an intermed

> ZFC hasn't been "replaced" by anything. My experience is the opposite: ZFC hasn’t been “replaced” in the sense that it never was - we always used an intermediate language of established theory which we compiled to ZFC. ZFC never formalized all of mathematics, as the high level congruences that drove category theory were always developed on an independent framework. Further, computers always were grounded in type theory and diagram equivalence (literally, the correspondence between circuit diagrams and type theories). > But the study of set theory has led to large number of metamathematical successes, such as forcing and the independence of the continuum hypothesis. Are there any which don’t exclusively apply to the mechanics of set theory itself? > The first two things you listed are not metamathematical statements. I noted fruits ranging from applied mathematics (eg, computer products) to meta mathematics; I think it’s important to understand applications as well. > OK, so what's the actual concrete statement an ordinary mathematician should be interested in? That the equivalence of algebra/geometry commutes with the equivalence of proof/computation has two practical effects: - we can encode proof engines as difference equations to run in GPUs - we can extract some “effective type theory” from difference equations interpreted as diagrams, which preliminary results suggest also relates to convolutions

spekcular 4y ago
Come on now. I just told in what sense ZFC has not been replaced, and you mentioned something different. No one ever claimed people actually wrote down their proofs in ZFC - again, that was never the purpose. > Are there any which don’t exclusively apply to the mechanics of set theory itself? Forcing has been applied to a variety of statements, including those about "normal" mathematics. The first example that comes to mind is the question of whether all automorphisms of the Calkin algebra are inner (Farah, 2011). There are many, many others. > That the equivalence of algebra/geometry commutes with the equivalence of proof/computation has two practical effects: You have still not given a statement an ordinary mathematician should be interested in! Type theory might good for engineering things - I'm totally on board with that. But if you claim HoTT has meta-mathematical interest, you need to give a meta-mathematical justification. That is, you need to prove something new (and interesting).
- zmgsabst 4y ago
  > I just told in what sense ZFC has not been replaced, and you mentioned something different. You told me your personal experience with textbooks and I told you mine. That’s how conversations work — why are you upset? You’re also factually wrong: I was pointing out areas of mathematics that (contrary to your claim) were never formalized in ZFC. > You have still not given a statement an ordinary mathematician should be interested in! I don’t think you’re being sincere at this point: the formalisms to accelerate reasoning engines and to extract semantic content of DNNs is of clear interest to many working professionals. - - - - - I think both threads have something in common: You’re dressing up your personal feelings (and ignorance) as grand statements about the field.
  - spekcular 4y ago
    It's an objective fact that the professional mathematical community has decided that ZFC is the standard foundations. The point of my post was not to explain my experience with textbooks, it was to note that you can check virtually any published source on this topic to find a reference for that claim. Extracting semantic content of DNNs is not a pure mathematical or metamathematical problem; it is an applied problem. Again, I'll happily admit type theory can be good for engineering stuff. But you claimed it was good for metamathematical inquiry. I'm looking for a statement about things like consistency, independence, shapes, numbers, etc. Set theoretical inquiry gave us tons of those, as I pointed out above.
    - zmgsabst 4y ago
      > It's an objective fact that the professional mathematical community has decided that ZFC is the standard foundations. This is factually untrue — there a portions of mathematics never formalized on ZFC and there’s not consensus around that. I listed the areas that weren’t formalized on ZFC already. You’re making bullshit up to make your personal biases sound grander than they are. - - - - > But you claimed it was good for metamathematical inquiry. No — you claimed that, as a strawman of my position. But you’re welcome to answer yourself: how do you formalize that equivalence is equivalent to equality without univalence? You’re on a huff, but never addressed the original point. From my very first post. > Extracting semantic content of DNNs is not a pure mathematical or metamathematical problem; it is an applied problem. Wrong. We lacked the meta mathematical framework outlining what semantics is to enable us to do that — until HoTT told us that the semantics of a system are in its topology. In that sense, HoTT is merely a fact about topos theory: the topology of your semantic model is the interesting part.
c-cube 4y ago
Is there actually any proof system running on GPUs?! I'd love to read about that. Afaict it must be super hard because tree manipulation is not great on GPUs...
- zmgsabst 4y ago
  Nope — research only I’m afraid; and currently just migrating to difference equations in numpy (with a focus on Numba GPU upgrades later). Currently moving shape types to digital image transforms; next up is Zn. https://www.zmgsabstract.com/whitepapers/shapes-as-digital-images https://www.zmgsabstract.com/whitepapers/shapes-as-digital-i... https://www.zmgsabstract.com/whitepapers/shapes-have-operations https://www.zmgsabstract.com/whitepapers/shapes-have-operati...
- raphlinus 4y ago
  Do not nerd snipe me! There's tons of juice left on the CPU side. Again I recommend Metamath Zero (which is somewhat of an opposite direction as HoTT), as it's able to check the entire Metamath proof database in a few hundred milliseconds. This is orders of magnitude faster than most other proof systems. If you did want to manipulate trees on the GPU, then my stack monoid work[1] might be a good basis for it. Of course, a whole nother direction is to use AI to develop proofs, which is a fascinating and growing area (see Holophrasm[2] and DeepMind work[3]). That of course runs on the GPU. [1]: https://arxiv.org/abs/2205.11659 https://arxiv.org/abs/2205.11659 [2]: https://arxiv.org/abs/1608.02644 https://arxiv.org/abs/1608.02644 [3]: https://www.deepmind.com/publications/proving-theorems-using-incremental-learning-and-hindsight-experience-replay https://www.deepmind.com/publications/proving-theorems-using...
  - zmgsabst 4y ago
    Would you be willing to elaborate on what you find to be strengths of Metamath Zero?

spekcular 4y ago

Come on now. I just told in what sense ZFC has not been replaced, and you mentioned something different. No one ever claimed people actually wrote down their proofs in ZFC - again, that was never the purpose. > Are there any which don’t exclusively apply to the mechanics of set theory itself? Forcing has been applied to a variety of statements, including those about "normal" mathematics. The first example that comes to mind is the question of whether all automorphisms of the Calkin algebra are inner (Farah, 2011). There are many, many others. > That the equivalence of algebra/geometry commutes with the equivalence of proof/computation has two practical effects: You have still not given a statement an ordinary mathematician should be interested in! Type theory might good for engineering things - I'm totally on board with that. But if you claim HoTT has meta-mathematical interest, you need to give a meta-mathematical justification. That is, you need to prove something new (and interesting).

zmgsabst 4y ago
> I just told in what sense ZFC has not been replaced, and you mentioned something different. You told me your personal experience with textbooks and I told you mine. That’s how conversations work — why are you upset? You’re also factually wrong: I was pointing out areas of mathematics that (contrary to your claim) were never formalized in ZFC. > You have still not given a statement an ordinary mathematician should be interested in! I don’t think you’re being sincere at this point: the formalisms to accelerate reasoning engines and to extract semantic content of DNNs is of clear interest to many working professionals. - - - - - I think both threads have something in common: You’re dressing up your personal feelings (and ignorance) as grand statements about the field.
- spekcular 4y ago
  It's an objective fact that the professional mathematical community has decided that ZFC is the standard foundations. The point of my post was not to explain my experience with textbooks, it was to note that you can check virtually any published source on this topic to find a reference for that claim. Extracting semantic content of DNNs is not a pure mathematical or metamathematical problem; it is an applied problem. Again, I'll happily admit type theory can be good for engineering stuff. But you claimed it was good for metamathematical inquiry. I'm looking for a statement about things like consistency, independence, shapes, numbers, etc. Set theoretical inquiry gave us tons of those, as I pointed out above.
  - zmgsabst 4y ago
    > It's an objective fact that the professional mathematical community has decided that ZFC is the standard foundations. This is factually untrue — there a portions of mathematics never formalized on ZFC and there’s not consensus around that. I listed the areas that weren’t formalized on ZFC already. You’re making bullshit up to make your personal biases sound grander than they are. - - - - > But you claimed it was good for metamathematical inquiry. No — you claimed that, as a strawman of my position. But you’re welcome to answer yourself: how do you formalize that equivalence is equivalent to equality without univalence? You’re on a huff, but never addressed the original point. From my very first post. > Extracting semantic content of DNNs is not a pure mathematical or metamathematical problem; it is an applied problem. Wrong. We lacked the meta mathematical framework outlining what semantics is to enable us to do that — until HoTT told us that the semantics of a system are in its topology. In that sense, HoTT is merely a fact about topos theory: the topology of your semantic model is the interesting part.

c-cube 4y ago

Is there actually any proof system running on GPUs?! I'd love to read about that. Afaict it must be super hard because tree manipulation is not great on GPUs...

zmgsabst 4y ago
Nope — research only I’m afraid; and currently just migrating to difference equations in numpy (with a focus on Numba GPU upgrades later). Currently moving shape types to digital image transforms; next up is Zn. https://www.zmgsabstract.com/whitepapers/shapes-as-digital-images https://www.zmgsabstract.com/whitepapers/shapes-as-digital-i... https://www.zmgsabstract.com/whitepapers/shapes-have-operations https://www.zmgsabstract.com/whitepapers/shapes-have-operati...
raphlinus 4y ago
Do not nerd snipe me! There's tons of juice left on the CPU side. Again I recommend Metamath Zero (which is somewhat of an opposite direction as HoTT), as it's able to check the entire Metamath proof database in a few hundred milliseconds. This is orders of magnitude faster than most other proof systems. If you did want to manipulate trees on the GPU, then my stack monoid work[1] might be a good basis for it. Of course, a whole nother direction is to use AI to develop proofs, which is a fascinating and growing area (see Holophrasm[2] and DeepMind work[3]). That of course runs on the GPU. [1]: https://arxiv.org/abs/2205.11659 https://arxiv.org/abs/2205.11659 [2]: https://arxiv.org/abs/1608.02644 https://arxiv.org/abs/1608.02644 [3]: https://www.deepmind.com/publications/proving-theorems-using-incremental-learning-and-hindsight-experience-replay https://www.deepmind.com/publications/proving-theorems-using...
- zmgsabst 4y ago
  Would you be willing to elaborate on what you find to be strengths of Metamath Zero?