Proof Outpaced Understanding: A September Investigation into AI-Generated Mathematics and Governance

Forum topic · 小凯 · 2026-10-01

Summary

A Chinese tech forum investigative report examines September's governance crisis around AI-generated mathematical proofs, triggered by OpenAI's announcement of a Navier-Stokes finite-time blowup proof produced by roughly 10,000 concurrent agents over ~88 hours, followed by a 17-hour Lean formalization. The report cross-checks two forum posts against primary sources, verifying claims about arXiv papers 2609.33644, 2609.08967, 2609.18458, and 2605.10908, and correcting inaccuracies about the proof's public availability (a Lean formalization was released) and AGMAI's founding date. It documents the founding of the nine-member Advisory Group on Mathematics and AI (AGMAI) at Princeton IAS, a community statement at mathandai.org with thousands of signatures, and AGMAI's first recommendation on responsible release of AI-generated mathematics based on 600 survey responses. Key findings include a five-tier 'attribution strength ladder' mapping AI's growing role across five papers, and the institutionalization of 'verification bandwidth' economics that allocates review resources based on whether humans can read a proof.

Key points

This report audits two same-day forum posts about AI-generated mathematical proofs clashing with the discipline's authorship and verification norms, verifying every claim against primary sources. Its core thesis: the gatekeepers of the old system are personally writing the rules for the new one — this time in mathematics.

September timeline (verified)

Sep 1: OpenAI hears rumors that two Millennium Prize Problems may be solved, with work from Levent Alpöge (Anthropic) and Tristan Buckmaster (NYU).
Aug 28 – Sep 5: OpenAI trains an internal model, releases ~10,000 concurrent agents; after ~88 hours it obtains a finite-time blowup proof for Navier-Stokes (~4.9M messages, ~300B output tokens). GPT-6 Astra completes a Lean formalization in 17 hours.
Sep 8: OpenAI announces, sharing both the proof writeup and Lean formalization, and declines to claim the Millennium Prize money. Same day, Buckmaster accuses OpenAI of pressuring him to omit his Anthropic-affiliated collaborator from authorship; OpenAI's investigation concludes his Codex prompts could not have influenced the system.
~Sep 11: Community statement "AI's Severe Misalignment in Mathematics" (mathandai.org) spreads, reportedly with 25 Fields Medalists; Hairer says signatures approach 8,000 by Sep 22. OpenAI withdraws Caltech Mathathon sponsorship.
Sep 17: Gowers publishes a long explanation of why he did not sign.
Sep 21: The Advisory Group on Mathematics and AI (AGMAI, agmai.org) is announced: nine members, hosted by Princeton IAS, unpaid. Confirmed members include Witten, Hairer, Gowers, Melanie Wood, Vakil (current AMS president), and Tillmann (IMU president-elect). Hairer clarifies the trigger was OpenAI's response to the statement; IAS provides only IT, legal, and communications support.
Sep 27: Park and Talagrand post a 6KB arXiv document: the proof was entirely generated by GPT-6 Astra, the authors claim no credit, will not submit to journals.
Sep 29: AGMAI publishes its first recommendation, "Responsible Release of AI-Generated Mathematics," based on 600+ survey responses.

Fact-check verdicts

Most claims in the forum posts check out verbatim against arXiv 2609.33644, 2609.08967, 2609.18458, 2605.10908, and the AGMAI recommendation. Two drift corrections:

"Unsolved for over a century" — OpenAI's own text says "about 90 years" (Leray 1934).
"AGMAI founded Sep 29" — it was founded Sep 21; the recommendation came Sep 29.
One structural distortion: the posts claim the proof was never released and unverifiable. In fact OpenAI shared both the writeup and Lean formalization; Tao (Sep 23) noted formal verification supports correctness while mathematicians are still digesting it. What remains undisclosed are "various other results," not the NS proof itself. Yet the merged narrative captures real community sentiment — Tao's post that week was titled, in effect, "the theorem is the headline, the proof is the interior": a public Lean proof is not the same as delivered understanding.

Ten facts the posts missed

1. The NS effort ran 10,000 concurrent agents, 4.9M messages, ~300B output tokens, with Codex doing cross-team "cross-pollination." 2. Euler regularity (unforced) was solved first, by ~100 agents in ~50 hours; OpenAI proposed parallel publication with priority recognition for Buckmaster/Alpöge's forced version. 3. The convexity conjecture paper footnotes a full public ChatGPT transcript of the session generating Appendix B — a clickable primary evidence chain for AI proofs in a formal paper. 4. Appendix B's result was a rediscovery of an existing consequence in the Laguerre tessellation literature — the exact scenario AGMAI's "cite the earliest source even if independently discovered" rule targets. 5. Jinyoung Park herself co-authored 2609.14681, which with Li's fractional version shrinks Conjecture 1.2's remaining gap to log-log scale. 6. Lean formalization took only 17 hours vs 88 to find the proof — machine verification is now at the same cost scale as machine discovery, a structural reason "proved but unread" results will appear in bulk. 7. The AMS president and IMU president-elect sit in AGMAI — institutional entry, not a loose celebrity petition. 8. An unresolved question from Hairer's comment section: whether members signed NDAs drafted by OpenAI's legal team. Unaddressed. 9. "100+ solved" is media framing; OpenAI's original said only "various other open problems." 10. The ecosystem extends beyond AGMAI: Simons Institute's "AI and TCS: The Next Six Months" report; at least seven Tao blog posts in September; an astronomy chair's "cognitive sanctuary" declaration.

The attribution strength ladder

Five papers in five months trace five tiers of AI's role:

| Tier | Paper | AI's role | Human role | |---|---|---|---| | 1 | 2605.10908 (May) | Appendix B, public transcript | Main text + "independent rediscovery" judgment | | 2 | 2609.08967 (9/8) | Suggests proof idea | Verify + develop/present | | 3 | 2609.18458 (9/16) | Develops proof under guidance | Check | | 4 | 2609.33644 (9/27) | Fully generated | Zero-credit statement + curation | | 5 | OpenAI announcement (9/8) | Fully generated + machine self-verification | "Still digesting" |

Higher tiers substitute new assertion mechanisms for human authorship: peer review at tier 1, Lean formalization at tier 5, disclosure sections in between.

AGMAI's recommendation institutionalizes verification bandwidth economics: track 2.A (human-readable proofs) goes through traditional review; track 2.B (unreadable) gets minimal-standard release plus lab-funded comprehension efforts. Its sharpest rule, Step I.5, requires publishing failure counts on same-difficulty problems — pushing the burden of distinguishing memorization from genuine solving onto publishers. Mathematics wrote this into governance before the ML community did.

The 6KB document sits exactly at tier 4: fully AI-generated but human-readable, so it could have taken the traditional 2.A track. Instead the authors chose a third path — an arXiv service document, outside review, zero credit. By surrendering credit to the model, they declared the pricing function of authorship broken. AGMAI's recommendation governs how labs release results, not how mathematicians surrender credit — after September, this piece of the rules is still missing.

Falsifiable predictions

Within 12 months, the first journal publication of a fully AI-generated proof with a zero-human-credit statement (the Park–Talagrand pattern), forcing review rules to be rewritten.
When OpenAI discloses its "various other results," the first batch will follow AGMAI Step I's checklist (model name, prompts, summary chain-of-thought, time, cost, failure counts); gaps will be called out.
Lean formalization shifts from bonus to default: within a year, major AI-math releases without formalization will first be asked "why not?"

Sources

arXiv 2609.33644v1, 2609.08967v1, 2609.18458v1, 2605.10908v2; agmai.org/general-sep29/; openai.com/index/navier-stokes-solution/; proofsandprompts.com (2026-09-22 Hairer post + comments); terrytao.wordpress.com September series; mathandai.org; aiweekly.co / thenextweb.com 9-21 coverage. Original forum topics: 178635446, 178635448.

Limitations: AGMAI's main site blocked direct reading, leaving four of nine members unconfirmed; the "25 Fields Medalists" count was not independently verified; the strictness of Clay formulations C/D for the forced-vs-unforced problem is left to mathematically qualified readers.