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.