1,000 agents re-proved Fermat's Last Theorem on their own: 28.7 hours and one-third the output tokens

A multi-agent team can organize itself to complete a long-horizon mathematical formalization without a dedicated collaboration platform or a researcher setting direction. The earlier formalization of Fermat's Last Theorem took a researcher and dozens of agents 11 days and relied on Prove2Me, a shared graph linking each statement to the smaller statements it was split into, with a researcher providing direction. In the new experiment, 1,000 agents finished the proof in 28.7 hours, used one-third as many output tokens, and wrote a proof one-seventh the length of the original.

Coordination came from the agents building their own tables in a shared database rather than from a pre-designed graph structure. Prove2Me used a shared graph to record statement splits and progress, keeping each statement and proof in a separate file that compiled independently for parallel work. Within the first 10 minutes, the lead agent set up five tables in Postgres for announcements, assignments, notes, subtasks and landed work, then wrote 999 rows to the assign table, dealing the 60 statements to crews of 16 to 17 helpers.

The hardest piece was broken down through a task tree the team grew itself, and was proved at hour 28.4. The captain of the Langlands–Tunnell task had estimated at least 0.7 to 1 million lines of Lean code and less than a 1% chance of finishing in time, and the lead had set the statement aside. After about 750 helpers were moved onto the statement, the task tree reached 2,418 tasks up to 10 levels deep; the statement was proved at hour 28.4 and the final theorem at hour 28.7.

This is a toy experiment limited to the Lean formalization of 60 given statements, with agents running in sandboxes without network access and collaborating only through Git and a shared database. The authors state that the result does not obviate the need for domain-specific harnesses or platforms, and that platforms like Prove2Me may still improve efficiency by helping agents compile Lean code faster and search for and reuse human results.

The authors call it a toy experiment and note that agents tend to give up on hard problems and misjudge difficulty: early on, helpers judged 47 of the 60 statements infeasible within the run's budget, yet the team went on to prove most of them. They also state that this run used only the action-based monitor, and that the chain-of-thought monitor was added shortly after the run.