[ripped_britches]

At this point we should make a GitHub repo with a huge list of unsolved “dry lab” problems and spin up a harness to try and solve them all every new release.

[abdullahkhalids]

There is in fact just such a repo maintained by Terence Tao and other mathematicians [1] who are actively using LLMs to try to find solutions to them.

[1] https://github.com/teorth/erdosproblems

[vessenes]

…and this problem was in fact sourced directly from that list!

[CSMastermind]

That's literally what the Erdős problems are. This post is about one of them being solved.

[josefx]

Except that Erdős problems are solved all the time, so many of them are already solved. Quite sure the last time I saw an article about an LLM solving an Erdős problem someone even tracked down a solution published by Erdős himself.

[7373737373]

This has existed for a few months, but there aren't any reports of (unsuccessful) attempts: https://github.com/google-deepmind/formal-conjectures

[johntopia]

that's actually a brilliant idea