4 ms·

Math follows a completely different approach with respect to how machine-learning AIs do their thing. Reason derives its strength in having a few primitives an

Math follows a completely different approach with respect to how machine-learning AIs do their thing. Reason derives its strength in having a few primitives and creating new assertions through the transformation of symbols by following precise rules (which is how algorithms work). In ML-based AIs, everything is imprecise and probabilistic, and this kind of generation gets its strength from building recognizable from utterly imprecise inputs and training - quite the opposite of how logic and reason evolve. Now, "classic" AI was a powerful way to derive new knowledge, and automatic theorem proving is a strong discipline; but the recent breakthroughs in AI are not directly applicable to classic techniques. Do you know what machine-learning AIs could be good for? Generating "insight" in problem solvers for guiding the theorem demonstrations through the proof search space, trying to find the best sub-spaces to explore. If there's a way to create human-like general AI, it will likely combine both kinds of generation - the rational methods of symbolic logic and the "irrational" statistical methods of ML.

zmgsabst 4y ago
Automated theorem proving is the same problem as “complete and label the diagram”, which image generation is okay at. Work in progress for sure, though.
- NateEag 4y ago
  > Automated theorem proving is the same problem as “complete and label the diagram”, which image generation is okay at. How so? I'm no mathematician, but I don't see how these problem types are equivalent. Could you elaborate?
  - zmgsabst 4y ago
    Sure — the connecting topic is topos theory. For a type theory we might want to reason about, there’s a diagram (in category theory) which represents the same semantic content. These diagrams turn out to have recurring and common structures. You can represent those diagrams as adjacency matrices, where those structures have a particular “shape” in the entries. Which if you squint hard looks like an image completion problem, ie, finding missing part of the matrix which represents a proof.
    - TuringTest 4y ago
      Who's using that topos theory, and is it well known in automated theorem proving? I hadn't heard about it before, although I have some notions of both category theory and theorem proving. And is your description of “complete and label the diagram” using image generation a thing that actually exists or something that has potential to be created? That could be a breakthrough in applying formal methods to real-world problems.
      - zmgsabst 4y ago
        Topos theory is used by people researching foundations, eg Michael Shulman. > And is your description of “complete and label the diagram” using image generation a thing that actually exists or something that has potential to be created? Somewhere between — it’s a topic being researched, but results are very early (basically, just shapes and groups).

zmgsabst 4y ago

Automated theorem proving is the same problem as “complete and label the diagram”, which image generation is okay at. Work in progress for sure, though.

NateEag 4y ago
> Automated theorem proving is the same problem as “complete and label the diagram”, which image generation is okay at. How so? I'm no mathematician, but I don't see how these problem types are equivalent. Could you elaborate?
- zmgsabst 4y ago
  Sure — the connecting topic is topos theory. For a type theory we might want to reason about, there’s a diagram (in category theory) which represents the same semantic content. These diagrams turn out to have recurring and common structures. You can represent those diagrams as adjacency matrices, where those structures have a particular “shape” in the entries. Which if you squint hard looks like an image completion problem, ie, finding missing part of the matrix which represents a proof.
  - TuringTest 4y ago
    Who's using that topos theory, and is it well known in automated theorem proving? I hadn't heard about it before, although I have some notions of both category theory and theorem proving. And is your description of “complete and label the diagram” using image generation a thing that actually exists or something that has potential to be created? That could be a breakthrough in applying formal methods to real-world problems.
    - zmgsabst 4y ago
      Topos theory is used by people researching foundations, eg Michael Shulman. > And is your description of “complete and label the diagram” using image generation a thing that actually exists or something that has potential to be created? Somewhere between — it’s a topic being researched, but results are very early (basically, just shapes and groups).