Comment by TuringTest
4 years 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.
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).