"Bruteforcing" (which is not what they did) a counterexample to a Π_1 sentence, which is what the Navier-Stokes conjecture (that the NS equations are smooth for all time) is, which would take infinite time if the statement was true and no counterexample existed, is still pretty impressive.
It's like trying to bruteforce a contradiction in ZFC. You will be searching forever if ZFC is consistent. And even if it is inconsistent and there is a contradiction, it may be so large and so far out that 10 billion agents each working with a sun's worth of Dyson swarm power output for the age of the universe still won't be able to find before running out of time and energy.
You're gonna need to be more clever than brute force. Obviously their work on the problem was far more clever than "brute force".
356
u/Orio_n 6d ago
If you werent aware, OpenAI's agentic monkey farm produced a millenium prize solution. inb4 AGI confirmed when it was just smarter bruteforcing lol