AI News

OpenAI Releases a Navier–Stokes Proof Claim: The Evidence and the Dispute

First published September 8, 2026. September 22 update: Kingy reviewed Clay’s September 11 statement and OpenAI’s September 10 investigation update. The detailed proof and participant-source review below remains dated through September 9, 08:41 UTC. This is a developing story based on public sources.

Current status: OpenAI’s claimed proof is public; Clay says the Navier–Stokes problem has apparently been settled and its evaluation will be unhurried. A manuscript and Lean formalization are available for scrutiny. Kingy has examined the stated result and supporting documentation without certifying the proof. OpenAI says its investigation ruled out influence from Buckmaster’s recent Codex prompts; Kingy has not audited private training records. Other allegations about research conduct remain contested.

OpenAI has moved the Navier–Stokes story from private reports to public artifacts. Its September 8 announcement links a 166-page manuscript, Finite Time Blowup for Navier–Stokes, and a Lean project. This is a substantial change in the evidence available to readers and mathematicians. It also makes the next question concrete: does the proposed proof establish the result it claims? OpenAI’s announcement on X, released paper, formalization repository.

Clay’s September 11 response: The Clay Mathematics Institute said the announced result has apparently settled the problem and welcomed its examination by mathematicians. Clay also said its prize evaluation process is deliberately unhurried and that it will provide updates. This is a significant institutional response, not a completed prize determination or Kingy’s independent proof certification. Clay’s statement, prize rules.

How the status changed on September 8: Earlier coverage, including Scientific American’s statement that the Clay formulation was solved, preceded the public proof located in this investigation. Our 16:41 UTC update therefore distinguished reporting from inspectable evidence. The manuscript is now available. Its release changes that assessment of availability, while examination of its correctness remains a separate task. Scientific American’s report.

The story deserves attention on several grounds: the mathematics, the growing role of AI in producing proofs, and a dispute about how research involving commercial AI systems should be credited and disclosed. Those questions need separate answers.

Here is what the principal developments actually concern:

DevelopmentWhat is publicly availableWhat it establishes at this stage
OpenAI: forced three-dimensional Navier–StokesA 166-page manuscript and public Lean projectA claimed resolution of Clay alternatives C and D, awaiting independent assessment in this report.
OpenAI: unforced three-dimensional EulerA separate 57-page manuscript and formalization in the same repositoryA claimed whole-space blowup proof from smooth initial data; distinct from the forced Navier–Stokes theorem.
Alpöge–Buckmaster: forced three-dimensional EulerA 112-page preprint and public Lean projectA claimed proof for Euler with smooth forcing; this is a different equation from Navier–Stokes.
Related Boussinesq and porous-media resultsA 76-page Boussinesq paper and 57-page IPM paper, alongside formalization materialsFurther results within the Alpöge–Buckmaster research program. The IPM paper also credits Matei P. Coiculescu as a coauthor.
Ganeshram and collaborators: unforced EulerA separate manuscript, numerical profile and 112-page stability companionA candidate singularity and conditional stability framework; a complete unconditional blowup proof remains unfinished.

The OpenAI rows refer to its released Navier–Stokes and Euler manuscripts and repository. The other results are described in the Alpöge–Buckmaster Euler, Boussinesq and IPM papers. The final row retains the qualifications on pages 13 and 67 of the separate Ganeshram–Duruisseaux–Anandkumar manuscript. Page counts identify the versions inspected.

The prize problem is about what the equations guarantee. Start with an admissible smooth three-dimensional incompressible flow: can a smooth solution continue for all future time, or can it break down? A singularity is a failure of the required mathematical regularity. Computing an approximate flow for an engineering application does not answer that universal question. Fefferman’s official problem statement.

There is a crucial detail in the rules. Options A and B ask for global smooth solutions with no external force, in ordinary three-dimensional space or a periodic domain. Options C and D allow a breakdown example with a smooth external force satisfying the specified decay and periodicity conditions. Consequently, a qualifying proof for forced Navier–Stokes could resolve a version of the Millennium problem. The force must obey the full assumptions; allowing it to become singular would evade the question. Official statement, page 2.

What OpenAI’s theorem says: For every positive viscosity, Theorem 1.1 constructs a flow initially at rest, driven by a smooth force compactly supported in space and time. Velocity becomes unbounded at a finite time while kinetic energy stays bounded. Corollary 10.6 supplies the periodic version, including periodic pressure. If the proof is correct, these stated conditions address Clay C and D. It does not claim unforced Navier–Stokes blowup. Theorem 1.1, Corollary 10.6.

The proposed construction centers on a contracting vortex. Its width shrinks faster than its length: both shrink, leaving an increasingly slender core. Oscillatory pulses and further corrections are designed to cancel singular errors so that the external force stays smooth even as velocity grows without bound. Controlling those cancellations with viscosity present is central to the argument. Physical explanation, pages 3–6.

Paper revision — September 8: The Navier–Stokes PDF now has 166 pages. Its expanded historical discussion credits Córdoba–Martínez-Zoroa’s earlier constructions, related work with Zheng, and classical wave-instability studies. The main theorem and periodic corollary are unchanged in our comparison. This documents expanded acknowledgment; it does not establish the authors’ reason for revising the paper or the origin of unpublished ideas. Revised introduction, pages 2–3.

OpenAI’s separate Euler PDF is now 57 pages. Its stated theorem scope matches the earlier version we read. Without a saved copy of that 45-page file, we have not established all changes between versions. Current Euler paper.

Euler removes the viscosity term. The Alpöge–Buckmaster Euler manuscript constructs smooth initial data and a force that remains smooth through the singular time, while vorticity—the local measure of rotation—becomes unbounded. Its geometry, regularity and forcing conditions are central to its claim. A headline that drops “Euler” or “with smooth forcing” changes the theorem being reported. Euler preprint, Theorem 1.1.

The Alpöge–Buckmaster program has a history. Diego Córdoba and Luis Martínez-Zoroa had already developed a program for constructing singularities by making different spatial scales interact. Their IPM preprint was first submitted in October 2024 and revised in February 2025. Their current work builds on that research. Córdoba–Martínez-Zoroa preprint.

For IPM, an important refinement is control of smoothness in both space and time. The new paper adapts the construction to a periodic domain and makes the forcing smooth in the joint variables. This distinction can disappear in a summary that calls both the earlier and newer forces simply “smooth.” The title alone is insufficient to compare the results. IPM preprint, introduction.

The Boussinesq paper gives a useful explanation of the mechanism. Begin with a background configuration that amplifies a small oscillation. The oscillation can have a small amplitude and a large gradient because its wavelength is short. Arrange for that stronger gradient to help amplify the next, even finer oscillation. Fit infinitely many stages into a finite interval, while controlling the unwanted effects introduced at each step. The hard part is making the gradients grow without losing control of the external forces or the rest of the equations. Boussinesq preprint, section 1.2.

In that construction, a relatively compact system of ordinary differential equations describes the central amplification mechanism. Turning it into a complete argument requires much more: localization, error corrections, derivative estimates and a consistent choice of scales. This helps explain why an attractive idea can still lead to a long proof. Boussinesq preprint, sections 1.2–1.3.

Earlier expert assessment: Before OpenAI’s public release, Tao described a plausible route from the Alpöge–Buckmaster program to Navier–Stokes, with enormous technical difficulties, and raised the possibility of eliminating forcing. That earlier assessment concerns a research direction. It should not be read as Tao’s endorsement of the newly released OpenAI manuscript. Tao’s follow-up.

Qualification on removing the force — September 8: Princeton mathematician Stan Palasek identified an obstacle to an unforced Navier–Stokes blowup built through instabilities at widely separated frequencies: in his argument, viscous energy loss would overwhelm the growth mechanism. Tao welcomed the observation and suggested studying a simpler model to make the interactions clearer. This concerns a specific proposed route to removing the force. It does not refute a forced Navier–Stokes result satisfying Clay’s assumptions, or settle every possible unforced approach. Palasek’s linked May paper studies a simplified shell model, rather than proving blowup for the full equations. Palasek’s observation, Tao’s response, model paper.

The missing evidence has changed. Readers can now examine a proposed Navier–Stokes proof. The next questions concern its mathematical estimates, its formal statement and the results of independent checking. A percentage-complete estimate would obscure those distinct tasks.

The human dispute begins with a more compressed chronology. Buckmaster dates the Boussinesq/Euler breakthrough to August 15 and Lean verification to August 22. He calls the collaboration personal, rather than an institutional Anthropic project. His statement also mentions an unreleased hypodissipative Navier–Stokes result whose Lean verification was unfinished. Buckmaster’s statement, page 1. Hypodissipative results concern a modified dissipation model and need their own classification. Euler preprint, related work.

Buckmaster’s account of the September 6 discussions: According to Buckmaster, during September 6 calls involving Sébastien Bubeck, OpenAI described an internal, roughly 100-page proof for forced Navier–Stokes under Clay options C and D. Buckmaster reports pressure over publication and authorship, including excluding Alpöge because of his Anthropic employment, and comments he understood as career threats. He also disputes the initial characterization of the amount of human input. Buckmaster’s statement, pages 2–3.

What his original statement did not establish: Buckmaster raised questions about access to their Codex drafts while explicitly saying he had not seen the internal proof and did not know whether their data had been used. The public release now allows examination of the mathematics; it does not by itself resolve the data-use question. Buckmaster’s statement, pages 3–4.

Bubeck’s response, expanded September 8: After his initial denial, Bubeck published a detailed account. He denies asking to remove Alpöge from authorship of Alpöge’s own work. He says the disputed discussion concerned Buckmaster leading a rewrite of OpenAI’s Navier–Stokes proof, and that Alpöge’s Anthropic employment made such participation inappropriate in his view. That is a distinction about which work and proposed authorship arrangement were discussed, rather than a resolution of every allegation. Initial response, detailed response.

Bubeck also acknowledges using language about risking a career, apologizes for the wording, and says he immediately retracted it. He characterizes it as concern about making unfounded accusations, while alleging that Buckmaster threatened to go to the press. These are conflicting accounts of the conversation and its intent; this investigation has not independently established what happened. Bubeck’s detailed response.

Alpöge and Bubeck’s exchange — newly incorporated: In September 8 posts at approximately 17:57 and 18:03 UTC, Alpöge says he would have welcomed collaboration and did not care about authorship on that step. He describes overhearing a call and interpreting what he understood as an offer involving the Millennium prize and his exclusion as meaning the outcome was fixed. Bubeck disputes that interpretation, saying discussions remained open and that Alpöge had not spoken with him. These posts predate our previous update but were newly reviewed for this revision. They supply conflicting participant accounts, without independently establishing the private conversation. Alpöge’s post, Bubeck’s reply.

Alpöge’s further account — September 9, 04:50 UTC: Alpöge says he contacted OpenAI on the night of September 2 to emphasize that his year-long collaboration was personal and used both Codex and Claude. He says he raised concerns about the company competing against mathematicians using its products and communicated an intention to decline marketing around the result. He also describes later assurances that OpenAI’s tools would be acknowledged. This adds his account of earlier contact to the disagreement with Bubeck described above. The post does not identify precisely whom he contacted or reproduce correspondence; it therefore does not independently settle that disagreement or establish access to unpublished work. OpenAI’s later investigation statement below is relevant. Alpöge’s new statement.

Sam Altman also backed Bubeck and described proposals for a coordinated release and a Buckmaster-led rewrite. His post adds the company leadership’s account; it is not independent corroboration of the disputed conversations. Altman’s response.

OpenAI’s company statement, updated September 10: OpenAI says verification preceded the September 6 discussions, that it offered access to its prompts and later its proof, and that it recognizes the pair’s forced-Euler priority. It denies that its researchers or agents saw the unpublished work or accessed specific user data for this problem. After an internal investigation, OpenAI now says Buckmaster’s Codex prompts from the preceding two months could not have influenced the system, including through training. That is the company’s reported finding; Kingy has not independently audited its model training or private data records. OpenAI’s updated statement.

Buckmaster has renewed his objection, pointing to OpenAI’s disclosure that the new model began training on August 28 and continued training during the effort. He interprets that timing as grounds for concern about customer data helping a lab overtake its users. The training dates alone do not establish the data cutoff or examples used. OpenAI’s later investigation statement is reported above; the underlying private records are not independently available to Kingy. Buckmaster’s September 8 response.

Buckmaster’s further objection — September 8, 21:32 UTC: Buckmaster renewed his criticism of OpenAI’s account of the research, referring to his team’s unpublished hypodissipative result and again raising concerns about training data. His post supplies no records establishing which material was used to train OpenAI’s models. OpenAI’s later investigation statement above is also relevant; use of the team’s unpublished work in training is not established by the sources Kingy reviewed. Buckmaster’s new post.

The citation dispute requires a version distinction: Buckmaster also attached a screenshot of Cao-Labora’s earlier criticism of missing references, posted at 18:08 UTC. Its pictured 16-entry bibliography matches the initial OpenAI Navier–Stokes paper retained in this investigation. The current 166-page version has 22 entries and includes Córdoba–Martínez-Zoroa and related work with Zheng. We found no bibliography entries for the Alpöge–Buckmaster collaboration, Chen–Hou or Elgindi in that version. In a 22:27 UTC follow-up, Cao-Labora acknowledged the added references while maintaining that relevant work was missing. At 22:44 UTC, he also acknowledged mixing up links in another exchange and said the bibliography shown there included key prior results. Our comparison here concerns the two saved Navier–Stokes versions specifically. These observations document a dispute over scholarly credit; they do not establish private-data use, misconduct or a mathematical defect. The older screenshot should not be read as the current reference list. Original criticism, acknowledgment of additions, link correction, current bibliography, pages 165–166.

Several questions follow, and none can be answered by counting reposts. Does a proposed proof work? How did the researchers and models arrive at it? What information did they have? What was said in the private conversations? A correct proof would answer the first question while leaving the others open. Conversely, a dispute over conduct would not establish whether the mathematics is valid.

The company has now supplied a dated research narrative and a description of human involvement. Those disclosures are useful evidence to assess, but they are not a completed independent provenance audit. Establishing which information reached which model or researcher would require records capable of answering that specific question. Similar methods alone cannot establish access to unpublished material.

Tao’s broader concern — September 8, 20:32 UTC: In a new thread, Tao argues that identifying fruitful questions is itself valuable research. He warns that enormous AI efforts triggered by hints of another group’s work could discourage researchers from sharing promising directions. He also criticizes the withholding of failed attempts and solution processes, and calls for standards that value mathematical insight alongside answers. This is an argument about research practices and incentives; it neither validates nor rejects the released proof or establishes misconduct. Tao’s discussion of incentives, proposed standards.

The original posts also need their historical context preserved. Deane Yang pointed to Buckmaster’s announcement; Emad Mostaque suggested OpenAI had already solved Navier–Stokes. Those posts helped circulate the story before OpenAI’s own release. They do not independently validate the proof now available. Yang’s post, Mostaque’s post.

Announcement chronology: Haider’s earlier post labeled an imminent announcement a rumor. OpenAI’s official proof announcement is now public, with the linked X post displaying September 8 at 10:20 a.m. Pacific / 17:20 UTC. That resolves the release question without establishing the proof’s correctness. Earlier rumor, official post.

Andrew Curran’s later post points to a separate Euler result. Its authors are Adarsh Ganeshram, Valentin Duruisseaux and Anima Anandkumar. Their approach uses a physics-informed neural network to find an approximate self-similar profile for Euler on unbounded three-dimensional space, without a boundary or external forcing. The work addresses a different set of assumptions using a different computational strategy. Curran’s post, authors’ announcement.

Conditional result, with proof work remaining: The manuscript reports numerical evidence and certified ingredients, alongside a conditional nonlinear stability framework. It identifies remaining quantitative certification work; it also states that an unconditional blowup result needs an appropriate existence and continuation argument. Tao’s added commentary describes completion of the stability argument within the residual-error tolerance as a major challenge. Calling this a completed unforced Euler proof would outrun both sources. Euler manuscript, pages 13 and 67, Tao’s updated exposition.

Separate Euler manuscript — newly inspected September 9: The authors’ Caltech project hosts a revised 107-page main paper, alongside the earlier copy linked above. We newly incorporated this version after comparing its expanded and reorganized discussion of stability and prior work. Its qualifications remain explicit: page 6 identifies numerical certification still needed, and page 14 says an unconditional blowup result also requires a local well-posedness and continuation argument. A revised exposition does not establish completion of those obligations. Current main paper, remaining work, continuation qualification.

Stability companion now available — September 8: A newly linked 112-page paper, Stability Framework for the Singularity of the Euler Equations on R3, is by Valentin Duruisseaux, Adarsh Ganeshram, Robert J. George and Anima Anandkumar. It sets out the proposed stability and reconstruction argument in detail. The abstract and remaining-work section still make completion conditional on rigorous certification of estimates and constants; page 28 explicitly says the stability proofs remain incomplete until suitable constants are certified. Availability of this framework is a substantive development, while the final certification remains unfinished. This review has not established a certified answer to Cao-Labora’s question below. Project page, companion, pages 1 and 5, certification qualification, page 28.

Stability companion revised — September 9 check: Compared with the version reviewed for our previous update, the 112-page companion adds a Chen–Hou reference and expands citations to earlier stability work. The changes identified in our text comparison are bibliographic; the paper still makes completion conditional on numerical certification. We found no newly reported certified derivative bounds resolving the question below. Expanded references, page 35, remaining work, page 5.

Expert question about the separate Euler candidate — September 8: EPFL mathematician Gonzalo Cao-Labora, a coauthor of earlier machine-learning research on fluid singularities, asked the Ganeshram–Duruisseaux–Anandkumar team to report bounds on the first and second derivatives of its equation residual—the error left when the approximate profile is substituted into the equation. His concern is that a small residual can coexist with much larger derivative errors, which matter when proving that a smooth solution lies nearby. He explicitly did not claim that their candidate has this problem and said he had not had sufficient time to study it. This is a concrete request for scrutiny, not an established error or a completed referee report. Cao-Labora’s comment, EPFL profile and research.

OpenAI’s account of the AI workflow: The company dates its effort to September 1 and reports roughly 10,000 concurrent agents, a result after 88 hours, and another 17 hours for Lean work using GPT-6 Astra. It describes reallocating agents, updating the internal model and feeding consolidated intermediate findings back into groups. These are company-reported figures and procedures. Research account.

The resource scale also matters. WIRED quotes OpenAI’s Mark Chen estimating that the compute expenditure ran into millions of dollars. This is a company estimate reported by WIRED, not an audited cost. WIRED’s report.

Bubeck separately says the human team lacked research-level expertise in fluid dynamics and could not meaningfully contribute mathematical content. That is his account of the division of labor. The disclosed orchestration still matters when interpreting claims of autonomous discovery: directing a large coordinated search differs from describing a single prompt and an unaided answer. Bubeck’s technical response.

AI’s role also requires a more precise vocabulary. In the IPM paper, the authors describe using Claude to work through prior literature and using Claude and Codex for drafting and the bookkeeping of constants and induction, under human direction. They describe their own adaptations and simplifications. This is a documented research workflow involving both mathematical judgment and model-generated work. IPM paper, discussion of language models.

The public Euler formalization’s README says Claude wrote the Lean code under Alpöge’s direction. It identifies a separate statement file and a comparator intended to check that the supplied proof establishes that statement. It also describes checks restricting the proof to the usual three foundational axioms used in classical Lean mathematics. These are concrete verification claims that other researchers can examine. This investigation inspected the documentation and theorem descriptions; it did not reproduce the large Lean build. Euler formalization documentation.

What the new Lean release establishes so far: OpenAI’s repository supplies Navier–Stokes and Euler formalizations plus instructions for a separate Comparator check. Its metadata labels the review status “self-assessed.” Checking instructions and available code are useful, inspectable evidence; they do not show that an outside group has successfully reproduced the checks. We inspected the documentation and theorem declarations, without running the build. Pinned repository, review metadata, checking instructions.

Lean matters because a proof checker can validate formal derivations under explicit assumptions. But the exact statement still matters, as do its definitions and dependencies. Lean’s documentation explains that additional axioms can undermine a proof and provides tools to audit them. For an article, “a formalization is available,” “an independent checker reproduced it,” and “experts confirmed that its statement matches the claimed theorem” describe different pieces of evidence. Lean’s documentation on axioms.

Physics-informed neural networks play another role: searching for candidate structures while penalizing violations of the governing equations. DeepMind and academic collaborators reported related work in September 2025. That history helps explain why the present moment contains several approaches, overlapping teams and different uses of the word “AI.” DeepMind’s 2025 research announcement.

The potential reward is mathematical understanding. A constructed singularity would reveal something profound about the limits of a particular idealized fluid model. It would not automatically supply a practical turbulence solver or immediate improvements in aircraft design. Those applications would require further work connecting the result and its methods to the problems engineers actually compute. Brown mathematician Javier Gómez-Serrano has emphasized both the promise of AI discovery and the substantial mathematics still needed to turn candidates into proofs. Brown’s August 26 interview.

There is also a distinction between mathematical acceptance and awarding the million dollars. Clay requires publication in a qualifying outlet, at least two years since that publication, and general acceptance by the global mathematics community before considering a proposed solution. An unchanged prize page cannot by itself refute a new proof; equally, a social-media announcement cannot substitute for the proof and its examination. Clay’s prize rules. OpenAI says it does not intend to claim the prize. OpenAI’s statement.

The next developments to watch are independent mathematical assessments, reproduced formal checks, revisions or corrections to the released proofs, substantive responses about research provenance, and completion or correction of the separate Euler stability work. Each update should identify which part of the evidence changed.

The story has advanced from a reported private claim to an openly inspectable proposed solution. Clay’s September 11 statement recognizes the apparent significance while reserving its evaluation process. Kingy has not independently certified the proof. OpenAI’s September 10 investigation statement narrows its account of possible data influence, but Kingy cannot audit the private records; the separate dispute over conduct remains contested.

Reporting method: Kingy.ai used AI research agents to review sources and assess updates. This revision examined the supplied manuscript and the official public release, including theorem statements, physical explanations, relevant proof qualifications, repository documentation and participant statements. We checked the main Navier–Stokes theorem and periodic corollary directly, including their rendered PDF pages. We did not independently verify every proof step, run the Lean builds or numerical certificates, interview participants, or audit private training records. This article is reporting and analysis, rather than an independent referee report.

Update policy: The initial four-hour monitoring window was scheduled through September 22, 2026. Material new evidence can warrant a further dated update: a substantive expert assessment, correction, direct response or change to the released proof. Repeated rumors and engagement alone do not. A check without new findings does not refresh the article’s evidence timestamp.

Update log — September 8, 2026: Initial publication. Separate checks of the mathematics and public dispute found no material change from the initial research. The article distinguishes public papers, unexamined private claims, conditional results, contested allegations and unanswered questions.

Update — September 8, 2026, 16:41 UTC / 9:41 a.m. Pacific: Added the Palasek–Tao exchange on obstacles to removing forcing, Cao-Labora’s qualified request for further checks of the separate Euler candidate, and clarification of Scientific American’s “solved” wording. The released manuscripts and formalization revision remain unchanged; this check located no public OpenAI Navier–Stokes proof. These additions report scrutiny and coverage, without upgrading the mathematical status.

Update — September 8, 2026, 18:20 UTC / 11:20 a.m. Pacific: Added OpenAI’s public manuscript and Lean release, the exact forced Navier–Stokes claim, its separate unforced Euler claim, and the disclosed agent workflow. Replaced the earlier no-public-proof status. Added the company’s qualified data-use response, Buckmaster’s renewed objection, Bubeck’s detailed explanation and apology, and Altman’s response. Proof availability is now established; independent acceptance and disputed provenance remain unresolved in this report.

Update — September 8, 2026, 20:48 UTC / 1:48 p.m. Pacific: Reported expanded historical acknowledgments in OpenAI’s revised Navier–Stokes paper and updated both OpenAI manuscript page counts. Added the separate Euler team’s conditional stability companion, Tao’s new research-practices argument, and attributed compute-cost context. Newly incorporated an earlier Alpöge–Bubeck exchange. The main Navier–Stokes claims remain unchanged in the comparison reviewed; independent acceptance and disputed provenance remain unresolved here.

Update — September 9, 2026, 04:48 UTC / September 8, 9:48 p.m. Pacific: Added Buckmaster’s later objection and the citation dispute, including Cao-Labora’s acknowledgment of added references and his link correction. Compared the pictured earlier bibliography with the current Navier–Stokes paper. Added the separate Euler stability companion’s expanded citations; its certification remains unfinished. OpenAI’s PDFs and the checked repository revisions remain unchanged. Independent proof acceptance and use of unpublished work in training remain unestablished here.

Update — September 9, 2026, 08:41 UTC / 1:41 a.m. Pacific: Added Alpöge’s new account of September 2 contact, clearly attributed and without treating it as independent confirmation of the disputed conversations. Newly incorporated the revised Caltech main Euler manuscript and its remaining proof obligations, alongside the earlier linked copy. OpenAI’s papers and the checked repository revisions remain unchanged. Independent proof acceptance and use of unpublished work in training remain unestablished here.

Update — September 22, 2026, 19:20 Pacific: Added Clay’s September 11 statement, which calls the announced result apparently settled and says its evaluation will be unhurried. Updated OpenAI’s data-use position to reflect its September 10 internal investigation statement about Buckmaster’s Codex prompts. These are attributed institutional and company statements. Kingy did not reproduce the Lean build, certify the mathematical proof, or inspect private training records for this update.

Featured image: AI-generated editorial illustration; not a simulation or proof visualization.