Work in progress for sure, though.
How so?
I'm no mathematician, but I don't see how these problem types are equivalent. Could you elaborate?
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.
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.
> 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).
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.