On October 26, 2026, OpenAI announced that its internal AI model had produced new research results in three fields: mathematics, computer science and physics. The results concern the local smoothing conjecture in harmonic analysis, the Exponential Time Hypothesis (ETH) in computational complexity, and existence proofs for quantum field theories, including quantum chromodynamics (QCD). None has been confirmed by independent peer review, so for now they remain claims made by OpenAI. The company had already published a large batch of mathematical results on GitHub on October 6, and a group of mathematicians based at the Institute for Advanced Study (IAS) has since issued a series of statements on how AI-generated research should be released. This time OpenAI asked outside experts for help and used a different release and verification approach for each of the three results, saying it does not yet know which approach is most useful. In practice, the three results differ greatly in what has been made public and what can be checked.
Three results, three release methods, different levels of verification
In this announcement, OpenAI described AI-generated manuscripts as a kind of "raw research data." To turn that data into scientific knowledge, it asked outside experts to act as "shepherds" and, where needed, to organize groups of researchers. Based on expert advice, however, the release method varies by field. In mathematics, the AI output is published as is, so researchers can verify and explain it on their own initiative. In computer science, an outside group of researchers was set up, while the AI output is also made public. In physics, an outside group was organized, and the decision on whether to publish the materials was left to that group.
Different release methods mean different materials are available to third parties. The comparison below therefore looks at three points: whether the AI-generated natural-language manuscript is public, whether formalization in the Lean proof assistant has been completed and a document explaining its scope has been published, and who decided on publication. It is based on OpenAI's announcement, two preprints and two documents describing the scope of the Lean formalizations.
| Field and OpenAI's claim | AI output and Lean formalization (per OpenAI) | Published materials | Outside group and publication decision |
|---|---|---|---|
| Mathematics: proof of the local smoothing conjecture in all dimensions, implying the Kakeya conjecture and others | AI output on October 18; Lean formalization on October 19 | Manuscript (59 pages, dated October 25) and Lean proof on GitHub | No outside group; published following the recommendation of experts consulted. Explanation and verification left to researchers' voluntary efforts |
| Computer science: refutation of ETH | Natural-language refutation on October 16; Lean formalization on October 17 | Manuscript (67 pages, dated October 17, revised on the 25th) and Lean proof on GitHub | A group of Impagliazzo, Paturi and Williams decided on immediate release |
| Physics: proof of existence of specific 4D quantum field theories including QCD, with an existence proof of pure Yang-Mills theory included | Natural-language proofs on September 9 (Yang-Mills) and September 18 (QCD). Lean formalization of the Yang-Mills existence proof completed on October 16 | Not public. No document showing the scope of Lean verification has been published, and nothing is stated about QCD formalization | A five-person group led by David Gross decided not to publish the AI's output and to write its own paper |
Of the three, both the AI-generated natural-language manuscript and the Lean formal proof have been published for two: the local smoothing conjecture in mathematics and ETH in computer science. For the Yang-Mills and QCD existence proofs in physics, the outside group decided not to release the materials. According to OpenAI, the natural-language physics proofs were generated on September 9, more than a month before the mathematics result (October 18) and the ETH result (October 16). Even so, as of October 27, the only thing outside researchers can consult is OpenAI's announcement.
That said, publishing a manuscript and a Lean formal proof does not guarantee that the result itself is correct. Lean checks whether a formalized statement is correctly derived from given axioms and definitions; whether that statement matches what the paper claims must be confirmed separately. For ETH, in fact, Lean's verification covers only standardly encoded inputs, and the proven running-time bound is weaker than what the paper claims. The scope document positions the result as exact counting in subexponential time, but whether it supports the paper's full claim requires separate verification. Even so, for the mathematics and ETH results, outside researchers can now begin their own verification from public materials.
How the "proof in all dimensions" of the local smoothing conjecture goes beyond earlier work
The local smoothing conjecture concerns how far the strong concentration of a wave at particular moments can be suppressed when averaged over time. OpenAI's explanation rests on the idea that even if a wave becomes extremely concentrated at some instant, that state does not last long, and the degree of concentration at a typical time is far smaller than in the worst case. The introduction of the published preprint gives an example in which a wave emitted from a thin spherical shell converges on a focal point, and the L^p norm, one measure of a wave's size, grows greatly relative to the initial state. The question posed by the mathematician Sogge is how much smoothness the initial data needs for this size, averaged over a time interval, to be bounded. Unlike estimates at the moment of greatest concentration, time averaging allows less smoothness to be required of the initial data, and that is the core of the conjecture.
The conjecture matters because it connects to other well-known open problems in mathematics. OpenAI explains that if the local smoothing conjecture holds, the Kakeya conjecture and Stein's restriction conjecture follow. The Kakeya conjecture, named after the Japanese mathematician Soichi Kakeya, asks how small a set in n-dimensional space can be if it contains a unit line segment in every direction. Specifically, it conjectures that the Hausdorff dimension of such a set, a dimension measuring its fine-scale spread, must be exactly n.
Research on these problems has advanced step by step from low dimensions. According to OpenAI, Sogge posed the local smoothing conjecture in 1991, and in 2020 Guth, Wang and Zhang published a paper in the Annals of Mathematics proving the case of two spatial dimensions. The paper appeared in volume 192, issue 2, pages 551–581, and went online on September 9, 2020. On February 24, 2025, Wang and Zahl also submitted a paper to arXiv claiming to show that three-dimensional Kakeya sets have both Minkowski and Hausdorff dimension 3. By contrast, the preprint OpenAI has now published claims in its abstract to prove the local smoothing conjecture in all dimensions with two or more spatial dimensions. According to the company, the proof uses a newly introduced auxiliary partial differential equation.
For the Lean formalization, the published scope document specifies what was verified. The target is the estimate bounding the L^p norm of the half-wave by the W^{s,p} norm of the initial data for all n≥2 and 2≤p<∞, with the smoothness exponent s=max(0,(n−1)/2−n/p)+ε for any ε>0. The formalization also includes an L^n estimate for the Kakeya maximal operator (with a δ^−ε loss) and the statement that a subset of R^n containing a unit line segment in every direction has Hausdorff dimension n. However, what Lean confirmed are these formalized statements; whether they match the claims of the whole 59-page paper requires independent verification by researchers. According to OpenAI, the AI generated the manuscript on October 18 and the Lean formalization was completed the next day. After consulting outside experts, the company chose, as on October 6, to publish the output as is and leave verification and explanation to researchers' voluntary efforts.
The ETH refutation claim, and the limits its own paper acknowledges
The Exponential Time Hypothesis (ETH) is a complexity-theory hypothesis that solving 3-SAT with n variables requires exponential time in the worst case. The preprint OpenAI published claims to present, for fixed k≥2, a deterministic algorithm that exactly counts the satisfying assignments of a k-CNF formula in polynomial space and subexponential time. If correct, this would be a counterexample to ETH, so OpenAI characterized the result as a refutation of ETH. According to the company, the AI generated the natural-language refutation on October 16 and the Lean formalization was completed the next day.
The paper itself, however, limits the scope of the result. Upper bounds of the subexponential form 2^{o(n)} are not necessarily preserved under general polynomial-time reductions, so even if the algorithm is correct, it would not mean that every NP problem can be solved in subexponential time. The document describing the scope of Lean verification also states explicitly that the formal proof covers only standardly encoded inputs, and the running-time bound proven there is weaker than the one claimed in the October 25 revision of the paper. Its comparison table organizes the Lean result as exact counting and SAT results in polynomial space and subexponential time. The fact that Lean verification has been completed therefore cannot be taken to mean the paper's whole claim has been proven. For the meaning of ETH and the difference between the bounds in the paper and in Lean, see XenoSpectrum's related article.
The group coordinating verification of the ETH result consists of Russell Impagliazzo and Ramamohan Paturi of UC San Diego and Ryan Williams of MIT. At the group's request, OpenAI agreed to publish all raw AI-generated data and to fund a conference discussing the implications for complexity theory as a whole. In an open letter to researchers, however, the three state clearly: "Our involvement should not be taken as certification of the claim." They are also seeking input from the research community on a proposal to hold an online meeting by the end of 2026. The group itself thus takes the position that the participation of prominent outside researchers does not mean the result has been confirmed.
How an existence proof for Yang-Mills theory differs from the Clay Institute's prize problem
In physics, OpenAI claims to have obtained a mathematically rigorous existence proof for certain interacting quantum field theories in four dimensions containing gauge fields and fermions. The targets reportedly include QCD and the simplest grand unified theory that completes the Standard Model of particle physics. The result also includes, as a sub-problem, an existence proof of pure Yang-Mills theory, which OpenAI describes as "part of" the Millennium Prize problem set by the Clay Mathematics Institute. As for why it targets a grand unified theory rather than the Standard Model itself, the company says the Standard Model cannot be extrapolated to arbitrarily short distances.
QCD and pure Yang-Mills theory differ in the range of interactions they treat. QCD describes how quarks and gluons interact through the strong force, whereas pure Yang-Mills theory deals only with interactions among the gluons that mediate the force. An "existence proof" here means rigorously constructing the theory as an object satisfying mathematical axioms. OpenAI explains that the proof builds on Balaban's work on constructive quantum field theory. However, the Clay Institute's Millennium Prize problem requires not only existence of the theory but also a proof of the "mass gap," meaning the lightest excitation has positive mass Δ>0.
The Clay Institute's official problem statement was written by Arthur Jaffe and Edward Witten. Comparing its requirements with OpenAI's announcement gives the following.
| Item | Clay Institute official problem statement | OpenAI announcement |
|---|---|---|
| Object of existence | A nontrivial quantum Yang-Mills theory on R^4 | Specific interacting 4D quantum field theories (such as QCD), including pure Yang-Mills theory |
| Standard required of the existence proof | Includes establishing properties at least as strong as a specified set of axioms | Claimed as a mathematically rigorous existence proof. Builds on Balaban's constructive field theory, but the axioms satisfied are not stated in the announcement, so this cannot be judged |
| Mass gap | Requires proof that Δ>0 | Not mentioned in the announcement |
| Range of gauge groups | Any compact simple gauge group G | Not described in the announcement, so this cannot be judged |
The Clay Institute asks for proof of both the existence of Yang-Mills theory and the mass gap for any compact simple gauge group. What OpenAI now claims is an existence proof for specific quantum field theories including pure Yang-Mills theory, and the announcement does not mention the mass gap. But because the body of the proof has not been published, it cannot be confirmed whether it contains any discussion of the mass gap or of the range of gauge groups. As for Lean formalization, OpenAI's explanation says only that the Yang-Mills existence proof was formalized on October 16; unlike for the mathematics and ETH results, no document stating the scope of verification has been published.
OpenAI also explained how the materials came to be withheld. According to the company, the AI-generated manuscript was long and complex, so it had planned from the start to delay release until Lean formalization was complete. After formalization was finished, OpenAI organized an outside group of researchers, in which David Gross, co-winner of the 2004 Nobel Prize in Physics, took on the coordinating role together with Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov. The group then decided not to publish the AI-generated materials and to write its own paper.
On October 26, AGMAI (Advisory Group on Mathematics and Artificial Intelligence), an advisory group of nine mathematicians based at the IAS, asked OpenAI to promptly release the natural-language proofs and Lean formal proofs in response to this decision. Its statement argues that the materials underpinning the existence proofs for Yang-Mills theory, QCD and the completion of the Standard Model should be understood in an environment equally accessible to all researchers. It also pointed out that, since OpenAI itself announced the completion of Lean formalization, there is no scientific reason to delay publication further. At the same time, AGMAI stated that it holds deep respect for the scientists OpenAI asked to coordinate, distinguishing its criticism of the release method from its assessment of the individual researchers.
What AGMAI objects to, and the Simons Foundation's $15 million in support
OpenAI set out four principles for its collaboration with outside researchers. First, participants are not asked to sign nondisclosure agreements, ensuring transparency so that they can discuss and publish freely, including intermediate results. Second, OpenAI itself does not seek academic credit for discoveries produced by its internal model. Third, groups of researchers who deepen understanding of the results should receive appropriate credit. Fourth, participation is voluntary and unpaid, and each member reaches research conclusions independently. OpenAI also acknowledges, however, that by choosing the initial coordinators itself, it creates a situation in which certain researchers get access to information first, leading to information asymmetry.
AGMAI had already taken a cautious position on such release methods. In its recommendations issued on September 29, it argued that the work of deepening understanding of AI-generated research results should be pursued voluntarily by the research community, not led by the AI company that produced them. It also recommended that decisions on which of these activities to fund should be made by independent nonprofit institutions, not by AGMAI or AI companies. On October 6, it also issued a statement saying that its having given advice should not be interpreted as an evaluation of OpenAI's research results or an endorsement of its methods.
In a further statement on October 25, it advised AI companies not to adopt in the future the approach of naming particular mathematicians and giving them priority access to materials. Its reasons included that disparities in access to information would arise among researchers, that selection could reflect relationships with the company or the company's priorities, and that the names of prominent mathematicians so designated could be used to deflect criticism of the company. It nonetheless credited the mathematicians named so far with pursuing valuable work in good faith. OpenAI announced these three results, using the approach of asking outside experts to coordinate, the day after that statement. AGMAI notes that its recommendations target mathematics and may not apply directly to other scientific fields, but its October 26 statement treats the Yang-Mills existence proof as an important mathematical problem as well.
Funding to support verification and understanding of research results also exists in two forms: a mechanism that distributes money through an independent nonprofit, and one in which OpenAI funds work directly. On October 15, the Simons Foundation announced that it, Anthropic and OpenAI would pool funds and resources for a total of $15 million (about 2.35 billion yen). The foundation manages the funds and selects grantees, and it will also run an open call. The proposal deadline for the call, the "Targeted Grants to Math+AI Institutes" program, is December 1, 2026. OpenAI says it will contribute $5 million (about 780 million yen) to the effort, and that money too will be managed and distributed by the Simons Foundation. The yen conversions use the October 23 exchange rate published in the Federal Reserve Board's H.10 release, 156.87 yen to the dollar.
In the announcement, Simons Foundation president David Spergel said that discussion of how to evaluate and use AI tools should be led by the mathematical research community, not by particular companies or institutions. By contrast, OpenAI has promised to fund directly the conference requested by the three researchers handling ETH verification. Both aim to support understanding of AI-generated results, but they differ in who holds the authority to decide how funds are allocated.
Verification of the three results will now proceed in different ways. For physics, the focus is on whether Gross's group publishes its paper, or whether OpenAI responds to AGMAI's request by releasing the natural-language proofs and Lean formal proofs. Once the materials are public, third parties will be able to check concrete details such as the mass gap and the range of gauge groups. For ETH, the online meeting by the end of 2026 on which the three are seeking input, and the conference OpenAI has promised to fund, will be occasions to gauge progress in verification. For the local smoothing conjecture in mathematics, no dedicated outside group has been set up, so what matters is how far researchers independently examine the 59-page manuscript and check it against the scope of Lean verification.
The results of the Simons Foundation call, closing on December 1, will also show which activities supporting the evaluation and understanding of AI-driven mathematics research receive funding. Whether verification of the three results announced now will be among the funded projects cannot be determined from the foundation's announcement alone. The physics result in particular concerns the rigorous construction of interacting four-dimensional quantum field theories, which AGMAI describes as a decades-old goal of mathematical physics. But to judge how far the claim actually resolves the problem, it is essential first that the content of the proof be made public and that outside researchers be able to verify it independently.
