41 ms·
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.
by pama 7d ago
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.
- 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.