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.