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.
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.