A Millennium Prize is awarded for an AI-produced proof

Where things stand (as of 15 Oct 2026)

• There is already a candidate solution. On 8 Sep 2026 OpenAI posted a 166-page paper credited only to "OPENAI", plus a Lean formalization. It establishes alternatives (C)/(D) of Fefferman's official Navier–Stokes statement: finite-time blowup with a smooth, compactly supported force. OpenAI's announcement says the proof was "produced by an internal OpenAI system". It also says "We do not intend to claim the Millennium Prize." (OpenAI; paper)
• The proof looks correct. The Lean statement was taken from DeepMind's Formal Conjectures repository and checked with the comparator tool (per a secondary write-up). Experts quoted by NPR think the result is correct.
  • The Bastounis–Circelli–Hansen preprint (arXiv 2610.08144, 6 Oct) shows the written proof and the Lean proof don't match. It does not dispute the Lean theorem itself.
  • Scientific American (14 Oct) reports the proof does not follow the Córdoba–Martínez-Zoroa program, so the credit sits mainly with the AI.
• CMI's position. Its 11 Sep statement says the problem "has apparently been settled". It adds that the rules govern "evaluating what has been achieved and for assigning credit" and that the process "is deliberately unhurried" (CMI). President Bridson has stressed peer-reviewed publication, but his recent remarks about working with AI are upbeat.
• The rules set a hard timeline (2018 rules):
  • The solution must appear in a qualifying outlet; CMI may relax the outlet conditions.
  • At least two years must pass after publication, with general acceptance.
  • A special advisory committee then reviews it.
  • CMI may give no prize if attribution or the appropriateness of an award is unclear.
• Headwinds. OpenAI does not submit its papers to journals. Two members of CMI's scientific advisory board, Donaldson and Okounkov, signed the Fields Medalists' letter "A Severe Misalignment of AI in Mathematics" (mathandai.org). The dispute with Buckmaster and Alpöge over credit is unresolved, and some experts call the forced version a "loophole".

Reference class and model

• Only one precedent. Poincaré: the first preprint was Nov 2002 and the award came 18 Mar 2010, about 7.3 years later and roughly 1.5–3.5 years after the published expositions (CMI 2010 release). CMI awarded Perelman even though he was expected to decline.
• How the estimate is built:
  • The proof holds up: about 0.97.
  • CMI eventually awards a prize recognizing the AI solution, alone or shared with earlier contributors (rule 8b): about 0.5.
  • Given an eventual award, it lands by end-2031: about 0.5. The two-year clock starts either from the Sep 2026 posting, if CMI relaxes the outlet rule, or from a 2027–29 journal paper or exposition. Then comes 0.5–2 years of committee work.
  • Authors' attribution of the proof to AI is restated after 16 Sep (OpenAI will restate it): about 0.95.
  • That gives about 0.23. Other routes (an AI solution to another problem in 2027, or a human team saying an AI produced the main proof) add about 0.03, for roughly 0.25 by end-2031.
• Hazard shape. Close to zero before the earliest two-year mark (Sep 2028); about 2% by end-2028; rising through 2029–31. Earlier quarters need CMI to waive its own rules.

Markets

• Polymarket, "CMI declares Navier–Stokes solved" (award or declaration, about $27K volume): 3% / 12% / 31% by end-2026 / 2027 / 2028. Because a declaration alone counts there, this is an upper bound for an award.
• Polymarket, OpenAI announces another Millennium solution by end-2027: 47%.
• Manifold, CMI "formally recognizes" OpenAI's proof before 2029: 75%, but a thin play-money market.

Strongest counterarguments

• For higher: CMI already wrote "apparently settled". The Lean check against a pre-existing community statement removes doubt about correctness. CMI has awarded a prize to someone expected to decline. AI may solve several more problems, giving more chances, and Bridson welcomes working with AI. That case points to 35–40%.
• For lower: CMI has only ever moved slowly. The mathematics establishment is hostile to the AI labs' conduct. There is no journal publication. OpenAI disclaims the prize and has no named human authors. The rules allow "no prize". That case points to 10–15%.

I weight these roughly equally.

Other sources

• Quanta, 8 Sep
• Wikipedia, priority controversy
• Scientific American, 21 Sep and 14 Oct
• NPR, 22 Sep
• AGMAI guidelines, 29 Sep
• TechCrunch, 8 Oct
• Polymarket market
• Manifold API (api.manifold.markets/v0/slug/...)

The quarterly hazards were compounded in Python; the cumulative series is in the forecast.

Question. By the last day of each quarter, has the Clay Mathematics Institute announced the award of a Millennium Prize for a solution whose authors state that an AI system produced the main proof?

Definitions.

• Millennium Prize: a prize awarded by the Clay Mathematics Institute (CMI) for a complete resolution of one of its seven original Millennium Prize Problems: Birch and Swinnerton-Dyer, Hodge, Navier–Stokes, P versus NP, Poincaré, Riemann, or Yang–Mills and Mass Gap. A disproof or counterexample counts if CMI awards the Millennium Prize for resolving the problem.
• Announce the award: an official CMI statement that it has awarded the prize or definitively selected its recipient(s). Acceptance, payment, and a presentation ceremony are not required. A shared award counts.
• Authors state: the solution's sole author, a jointly authored paper or statement, or an identified author explicitly speaking for the author team attributes the main proof to AI. An individual coauthor's statement solely about their own contribution does not suffice. The attribution must concern the solution recognized by CMI, not a different proof of the same result.
• AI system produced the main proof: the authors explicitly say that an AI system generated the proof as a whole or the principal mathematical argument establishing the result, rather than merely assisting with it. Equivalent descriptions such as “the proof was primarily AI-generated” count. Human selection of the problem, prompting, supervision, use of prior human mathematics, verification, editing, and correction do not disqualify the solution if the authors still make this attribution. An AI system may comprise multiple models or agents and may be developed by any organization.

Resolves YES if both a qualifying CMI award announcement and a qualifying author attribution are publicly available by the quarter-end. The attribution need not appear in the award announcement, and CMI need not endorse the attribution. If attribution appears after the award announcement, the qualifying date is the publication date of that later attribution. Both required publications must satisfy the Resolution window; a new qualifying statement may expressly reaffirm an earlier attribution.

Exclusions (resolve NO).

• A proposed solution, journal acceptance, formal verification, widespread mathematical acceptance, CMI review, an advisory recommendation, or an announcement of eligibility without an actual award decision.
• A Clay Research Award, a smaller award for partial progress or a counterexample that leaves a reformulated problem unresolved, or any prize other than a Millennium Prize.
• Attribution only of literature searches, calculations, experiments, isolated supporting lemmas, exposition, translation into a proof-assistant language, or proof checking to AI; “AI-assisted” without explicit attribution of the principal argument is insufficient.
• Credit inferred by commentators or asserted only by an AI vendor that is not speaking as an author of the recognized solution. Independent verification of the authors' AI attribution is not required, but an attribution expressly withdrawn before the two conditions are first satisfied does not count.

Resolving source. The award must be announced on claymath.org or in a CMI-authored official announcement. CMI's Millennium Prize Problems page and Millennium Prize Description and Rules, dated 26 September 2018, identify the prizes; CMI's award decision controls even if it subsequently changes its eligibility rules. Author attribution must be in the solution paper or its supplementary material, a signed author statement on an author or institutional website or scholarly repository, or an author statement quoted in CMI's announcement. These are the question-specific sources rather than the broader Public confirmation (A2) source set; interviews, social-media posts, and press paraphrases do not substitute. Apply Resolution date (A3) to the later of the two required publications, and apply the Resolution window and its once-YES rule.