Not only that, but it used 10k agents coherently over 88 hours to come up with the proof. This is a significant advance.
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.
What makes you think they were coherent?
alt Hacker News
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.