9 ms·
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
by danielmarkbruce 8d ago
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.
- pama 7d agoAs far as I understand the 10k agents worked on the proof. The lean formalization came later and was easier/faster than getting the proof.
- danielmarkbruce 5d agoYeah, 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.