Hacker News Reader

Comment by pama | Hacker News Reader

Not only that, but it used 10k agents coherently over 88 hours to come up with the proof. This is a significant advance.

View on HN

With 10,000 agents and $20M of compute this is just brute force search.

It's a bit like telling 10,000 kids there's an easter egg hidden over there, pointing to one corner of your yard (or having "heard a rumor" it was hidden in that corner).

If you have $20M to spend on your problem, then yes, AI brute force search is an option, but unless you know a solution is possible (as OpenAI did here), you may still be wasting your money.

You jest and that is OK. Brute force search is not something you can do over math problems of that difficulty or anything with combinatorial complexity.

To me it feels closer to taking the top 10k human mathematicians on a large retreat for a year and having them self organize to collectively solve this problem—not kids and easter eggs.

I'm not joking. Compare to a super-human MCTS system like AlphaGo or Stockfish - once you condense the expertise of your top 10K world experts into a board evaluation or policy function, then the rest is brute force.

Whether this type of agentic swarm approach can be considered closer to MCTS (search), or closer to a less structured GOFAI blackboard type approach (perhaps more like your mathematician retreat) I'm not sure - I don't think they've released any details of the prompt(s) and how these agents were collaborating and building on each others work.

The other part of my easter egg analogy is the direction to "look over there", corresponding to OpenAI specifically asking their hoard of mathematicians to work on Navier-Stokes since they knew it was solvable/determinable, and they certainly had the public work that Buckmaster/Levant were building on as further direction, as well as perhaps their prompts. Unlike Buckmaster/Levant, this wasn't just a couple of humans with a university research grant budget, this was apparently a not-so-small team at OpenAI (says Buckmaster, per a group call he had with OpenAI), with an unlimited budget, so it's hardly surprising (or in the least bit impressive) that they were able to duplicate and surpass their work.

I agree with search, which is what mathematicians also use over longer periods of time. But it is not brute force search (and neither is alphago’s search or modern stockfish, though both still search at depth and speed higher than typical human).

If you can create a graph of independent work, which you can with many such problems, agents can work together nicely. Again, thank Lean and the tooling around it.

As far as I understand the 10k agents worked on the proof. The lean formalization came later and was easier/faster than getting the proof.

Yeah, good catch. I was under the impression they did the proof in lean from the get go, but you are right.

I guess the nature of the problem lent itself to the 10k agents. Ie, there isn't something general to take here.

What makes you think they were coherent?

They managed to solve a problem that was beyond current human ability.

That was the net effect (assuming what they solved was the actual problem and not a loophole in the problem statement or a lean bug). My point is they need not all work coherently to do that -- for example, for all we know 3/4 of them went off the rails, their results were pruned, and the relevant results came from a random subset that happened to produce something useful.

If you work with distributed systems, you still call that scenario a success. On the other hand, if the 3/4 of agents going off the rails bring down the whole mission, that is a failure. The latter would have been my guess with current models scaling to 10k agents.

I am not an expert in lean4, but I could follow parts of the high level lean definitions of the problem statement in the repo. A lean bug would be a fun scenario; I am certain this proof will receive the deserved scrutiny, and if it uncovers a bug, it will make the story even more exciting. It is extremely unlikely to be the case, however, because the 10k agents working on the proof didnt use lean, so it would have to be a math logic error that translates to a lean bug—perhaps something the agents picked up during training?

Reply on news.ycombinator.com