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

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.

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.

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