How far we have come :.)
SOME of the problems that have eluded humans are going to turn out to be low hanging fruit that are susceptible to this type of brute force (10,000 agents on a supercomputer running for 7*24 hours straight) AI search.
I'd be more impressed if OpenAI found their own problems to solve, rather than rushing in to re-solve one once they heard it was already solved (and therefore not so hard).
Magnus Carlson had a peak ELO rating of almost 2900.
Would you be impressed with someone with an ELO of 3700?
Would you still be impressed if I told you it was Stockfish?
OpenAI didn't go looking for a tough-for-an-AI problem to solve - they went looking for one that looked like it was easy since it they had heard it had already been solved.
Do you find this impressive?
But, I assume the Stockfish developers aren't comparing themselves to Magnus.
Let's see if OpenAI, or someone else, can get these sort of physics/math results out of a desktop PC - that would also be an impressive piece of engineering!
Not exactly...
From here:
https://cims.nyu.edu/~tristanb/statement.pdf
"I was shown a prompt and told the internal research model had simply been given the problem statement. Levent had been told by Sebastien “very little human input” had been used. This turned out not to be true. Over the course of the call, as members of their team sent Sebastien corrections and details over their internal chat, it emerged that an entire team had been working on the problem".
- OpenAI lying their face off for marketing purposes
- Buckmaster sore about getting beaten to NS, misrepresenting what was told
- Buckmaster not being an expert in ML, not understanding what he was told and hearing what he wanted to hear as it vindicated him
- Others...
OAI claimed that none of the people on their team were domain experts. So it's more akin to Deep Blue than Stockfish (actually slightly better than Deep Blue which did hire domain experts) but nevertheless represents a highly sophisticated automatic theorem prover.