OpenAI says roughly 10,000 concurrent agents worked for about 88 hours on the successful search, followed by additional Lean formalization and verification.
OpenAI reports that a large coordinated-agent system produced a finite-time singularity construction resolving statements C and D of the Navier–Stokes Millennium Prize formulation, together with a Lean formalization.
OpenAI says roughly 10,000 concurrent agents worked for about 88 hours on the successful search, followed by additional Lean formalization and verification. Independent reporting corroborated the publication event while also documenting disputes over attribution, provenance and priority involving contemporaneous work by Tristan Buckmaster and Levent Alpöge. OpenAI now says that, following an investigation, Buckmaster's Codex prompts during the two months before the 8 September release could not have influenced the system in any way, including through training. That direct statement narrows one provenance concern, while separate disputes over attribution, priority and the collaboration process remain part of the public record.
Because the claim concerns a Millennium Prize Problem and immediately triggered broad independent scrutiny and controversy, the event is historically significant regardless of the claim's eventual mathematical disposition. The proof, priority, attribution and community reception remain subjects for external mathematical and historical assessment.
Significance rationale: A publicly released AI-generated claimed solution to a Millennium Prize Problem is intrinsically a historical AI4Math event regardless of whether the underlying mathematical claim ultimately survives review. H1 records the magnitude of the event; verification separately records independent corroboration, dispute and later changes in the historical record.
—
The Chronicle records this event from the cited primary or official source; the status does not imply independent Chronicle verification.
Independent reporting corroborated the core event facts that OpenAI publicly announced the claimed Millennium Problem solution, released a proof manuscript and Lean formalization, and described the large multi-agent search. This event-level corroboration does not certify the underlying mathematical claim.
The Chronicle confirmed the public 166-page proof manuscript and Lean 4 repository formalizing the Navier–Stokes and Euler results. These primary artifacts strengthen the evidence record and support machine-checked formal assurance; independent mathematical assessment of the underlying claim remains a separate question from event-level corroboration.
Reliable independent reporting also documented material disputes over attribution, provenance and priority involving contemporaneous work by Tristan Buckmaster and Levent Alpöge. The Chronicle therefore records the event as `disputed` while preserving that the publication event itself is independently corroborated.
Axios independently documented Buckmaster and Alpöge's provenance and credit concerns and reported OpenAI's then-public boundary: the company said it did not access their specific user data for the proof, while acknowledging uncertainty about whether de-identified product-usage data could have indirectly improved its models. This sharpened the provenance record without establishing that such indirect use occurred.
OpenAI's current public account states that, after an investigation, Buckmaster's Codex prompts during the two months before the 8 September announcement could not have influenced the system in any way, including through training. This materially narrows the previously recorded prompt-training provenance uncertainty. The event remains `disputed` because the broader public record still contains separate attribution, priority and collaboration-process disputes. The French Mathematical Society's 15 September position also documents continuing institutional concern around the episode without independently adjudicating the underlying proof.
Clarified the title to describe OpenAI's publication as a claimed solution rather than as the Chronicle's own adjudication, and recorded the independently reported attribution/provenance dispute.
