News for hackers. Stuff that matters.
Re:AI Language Models Are Struggling to “Get” Math by TuringTest on Thursday October 13, 2022 @04:33AM (#33188629)
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.

Re:AI Language Models Are Struggling to “Get” Math by zmgsabst on Thursday October 13, 2022 @08:11AM (#33189904)
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).