If you can create a graph of independent work, which you can with many such prob...

pama · 2026-09-10T03:01:47 1789009307

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 · 2026-09-11T19:17:13 1789154233

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