Agent swarms reproduce formal proofs

A 1,000‑agent Fable 5.2 snapshot coordinated to reproduce a Lean formalization of Fermat’s Last Theorem in ~29 hours using supplied theorem statements, a route sketch, and 47 lemmas. This was run with significant starting scaffolding (60 statements, 47 lemmas) and contrasted with single‑model runs that stalled, showing coordination is the differentiator, not raw single‑model ingenuity. — If agent teams can reliably carry out formal mathematics with human‑supplied scaffolding, that shifts where we expect automation to appear in research and raises questions about verification, attribution, and governance of machine‑authored formal results.