AI Agents Collaborate for Four Weeks to Produce New Math Results for $3,000 in GPU Costs

On September 15, Dimitris Papailiopoulos announced that a piece of mathematical research completed through 4+ weeks of collaboration among multiple AI agents—Astra, Sol, and Fable—was about to be released. He said his own role was limited to asking questions and paying roughly 3000 USD in GPU costs, with the draft and about 100GB of verification "certificates" to be made public the next day. The credibility and formalization feasibility of the proof became the topic of a discussion with researchers including QuangVDao, making this the latest flashpoint in debates over trust in AI-assisted mathematical research.

Confirmed

• The project was carried out by three models—Astra, Sol, and Fable—working as agents in collaboration for over 4 weeks; Papailiopoulos described his role as only asking questions and paying the bills, with the 3000 USD GPU cost spent mostly on computing lower and upper bounds in parallel.
• He will release the draft along with roughly 100GB of certificate files; the mathematical reduction part of the proof is presented in elementary form, and the numerical premises are explicit finite inequalities that can be independently checked.
• On the tech stack, no harness optimization was done—the setup used stock Codex and Claude Code, letting the models communicate and hand off tasks to one another; he admitted the process was extremely messy, with reproducible results but a process that is hard to replicate.

Unconfirmed

• The correctness of the proof itself has not been peer-reviewed; Papailiopoulos said the results were cross-checked via hundreds of agent calls spanning 3 models, and claimed he has never seen a case where these models declared a proof correct only to be refuted—though QuangVDao and others remain skeptical of this verification approach.
• QuangVDao questioned whether such certificates could feasibly be encoded and checked in Lean; Papailiopoulos argued the proof consists of many different inputs, bounds, and numerical tables with poor compressibility—taking forms like "if the chosen probability distribution and numerical tables satisfy all specified inequalities, then the capacity upper bound equals a certain value"—so formalizing in Lean may not simplify things.
• Papailiopoulos also acknowledged one technical caveat: proofs that pass the verifier still have limitations (see his original wording for specifics).

Why it matters

• Producing new mathematical results with roughly 3000 USD in GPU costs over four weeks, the project demonstrates the low-cost viability of multi-agent collaborative research.
• The route of "hundreds of cross-validating agent checks replacing Lean formalization" challenges traditional standards for proof credibility, and its release of a 100GB independently checkable certificate could set a precedent for future AI-assisted proofs.

2026-09-15 ~ 2026-09-15 · 10 related posts

• [source] Dimitris teases 4-week collab dropping tomorrow: ~100GB of certificates for $3k in GPUs — DimitrisPapail · 2026-09-15
• 4-week three-model AI math collab yields ~100GB of certificates for $3k in GPUs — QuangVDao · 2026-09-15
• AI agents spend 4 weeks and $3k in GPUs to produce a new math result — giannis_daras · 2026-09-15
• [source] Where the $3k GPU budget went: parallelizing bounds in an AI-agent math study — DimitrisPapail · 2026-09-15
• No harness optimization: agents just talked to each other via vanilla Codex and Claude Code — DimitrisPapail · 2026-09-15
• Massive AI-generated numerical certificates resist Lean encoding — DimitrisPapail · 2026-09-15
• Why encoding massive numerical-certificate proofs in Lean is impractical — QuangVDao · 2026-09-15
• Cross-verifying AI math proofs with hundreds of agent calls instead of Lean — DimitrisPapail · 2026-09-15
• [source] AI-assisted math proof cross-verified by hundreds of agent calls, 100GB checkable file to come — DimitrisPapail · 2026-09-15
• Computer-assisted proof debate: author to release 100GB of independently checkable verifications — DimitrisPapail · 2026-09-15