Hacker News Reader

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.

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.