OpenAI Asks Outside Experts, Including Nobel Laureate, to Verify AI-Generated Proofs in Math, Computer Science and Physics

OpenAI has recruited independent experts to examine major scientific results produced by its internal AI models, marking a new stage in the company’s efforts to use artificial intelligence for advanced research. Announced on October 26, 2026, the initiative covers three areas: harmonic analysis in mathematics, computational complexity in computer science and the mathematical foundations of quantum field theory in physics.

The effort includes a team led by Nobel laureate David Gross for the physics result and computer scientists Russell Impagliazzo, Ramamohan Paturi and Ryan Williams for a claim involving the Exponential Time Hypothesis. OpenAI says its models produced proofs of results that researchers have struggled to establish for decades. However, these claims still require independent examination, and the company is experimenting with different ways to publish and verify the work rather than presenting all three as settled scientific breakthroughs.

Key Takeaways

• Independent verification: OpenAI has asked outside researchers to examine three major results generated by its internal AI models.
• Computer science: The AI claims to have disproved the Exponential Time Hypothesis, a conjecture underpinning hundreds of conditional hardness results.
• Mathematics: OpenAI says its models proved the local smoothing conjecture in every dimension, with implications for the Kakeya and Stein restriction conjectures.
• Physics: A team led by Nobel laureate David Gross will examine a claimed existence proof for certain four-dimensional quantum field theories.
• Lean formalization: OpenAI has formalized the mathematics and computer-science proofs in Lean, a system that checks formal mathematical arguments.
• Not yet independently confirmed: The scientific significance of the claims depends on experts validating the proofs and their interpretation.

Why OpenAI Is Asking Experts to Check Its AI’s Proofs

AI systems are increasingly being used to explore mathematical problems, develop algorithms and assist scientific research. But producing a proof is different from generating a plausible explanation or passing a benchmark.

A mathematical proof must establish a conclusion through a chain of valid logical steps. In advanced research, it must also address the precise assumptions, definitions and conditions of the original problem. A long, technically sophisticated manuscript can still contain a gap or prove a statement different from the one researchers intended.

OpenAI says its AI-generated manuscripts should initially be treated as raw research material. The goal is to give specialists the opportunity to understand the arguments, test the claims and explain their significance within established research.

The company has adopted three approaches for its October 26 release. The mathematics proof and its Lean formalization have been published for researchers to examine. The computer-science result is being reviewed by an external group, with its underlying materials made public. For physics, OpenAI is allowing the outside team to determine how the result should be presented.

OpenAI says the collaborations are voluntary and unpaid, with researchers free to discuss their findings and publish their conclusions. The company also announced a $5 million contribution to the Simons Foundation to support workshops, conferences and research programs focused on understanding AI-generated scientific results.

1. AI Claims to Disprove the Exponential Time Hypothesis

The computer-science result is potentially significant because it challenges a widely used assumption about computational complexity.

The Exponential Time Hypothesis, or ETH, concerns how quickly computers can solve certain Boolean satisfiability problems. These problems ask whether a logical formula can be made true by assigning values such as true or false to its variables.

As the number of variables increases, the number of possible assignments can grow exponentially. The ETH proposes that certain satisfiability problems cannot be solved substantially faster than the expected exponential-time limit.

Researchers have relied on this hypothesis to establish conditional lower bounds for hundreds of problems across graph theory, computational biology, databases and computational geometry.

OpenAI says its AI system produced a deterministic algorithm that contradicts the hypothesis. If the proof holds, researchers would need to revisit many results that depend on ETH being true.

However, this would not automatically solve the P versus NP problem. ETH is a conjecture about the difficulty of solving particular problems, while P versus NP asks whether every problem whose solution can be checked efficiently can also be solved efficiently. Disproving ETH does not establish that P equals NP.

The independent review will be led by Russell Impagliazzo and Ramamohan Paturi of the University of California, San Diego, and Ryan Williams of the Massachusetts Institute of Technology. Impagliazzo and Paturi helped formulate the hypothesis, while Williams is known for research connecting algorithms and computational lower bounds.

OpenAI has published the natural-language proof and Lean formalization for public examination. The reviewers will assess whether the argument is correct and what it would mean for computer science.

2. A Claimed Breakthrough in Harmonic Analysis

The mathematics result concerns the local smoothing conjecture, proposed by mathematician Christopher Sogge in 1991.

The conjecture addresses the behavior of waves and how their concentration changes over time. In simplified terms, extreme wave concentration may occur at particular moments, but averaging the behavior over time can produce stronger regularity than examining the worst instant alone.

OpenAI says its models produced a proof of the local smoothing conjecture in every dimension. According to the company, the result also establishes the Kakeya conjecture and Stein’s restriction conjecture in all dimensions because those results follow from the local smoothing statement.

The significance lies in the breadth of the claimed result. Researchers had previously established important special cases, including the local smoothing conjecture in two spatial dimensions in 2019 and the Kakeya conjecture in three dimensions in 2025.

OpenAI reports that its system produced the natural-language proof on October 18, 2026, followed by a Lean formalization the next day. The company has released both for the mathematical community to examine.

Unlike the computer-science result, this proof does not have a dedicated external verification group publicly coordinating its review. OpenAI says it consulted an outside expert and followed advice to publish the materials directly so researchers could organize their own examination.

3. A Physics Proof Involving Yang–Mills Theory

The third result concerns the mathematical foundations of quantum field theory, which physicists use to describe elementary particles and their interactions.

OpenAI says its AI produced an existence proof for certain interacting quantum field theories in four dimensions, including quantum chromodynamics (QCD) and a unified completion of the Standard Model of particle physics. The work also includes an existence result for pure Yang–Mills theory, which is connected to one of the Clay Mathematics Institute’s Millennium Prize Problems.

Yang–Mills theory describes interactions involving gauge fields. In the case of the strong nuclear force, gluons carry the force that binds quarks together inside protons and neutrons.

The distinction between an existence proof and a complete solution to the Millennium Prize Problem is crucial. The official Yang–Mills problem also requires proving the existence of a mass gap, a property associated with why the theory’s lowest-energy excitations have a positive mass. OpenAI has not claimed to have resolved that second requirement.

The physics review will be led by David Gross, who shared the 2004 Nobel Prize in Physics for his work on asymptotic freedom. The team also includes Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov.

For this result, the group has chosen to withhold the AI-produced materials while working on its own write-up. OpenAI says the goal is to produce a clearer and more useful scientific account of the work.

How Lean Helps Verify AI-Generated Mathematics

Lean is a proof assistant: a software system that checks whether a formal mathematical argument follows from explicitly stated definitions and assumptions.

A conventional research paper is written in natural language, which allows mathematicians to communicate ideas efficiently but can leave room for ambiguity. A formal proof translates the argument into a precise structure that Lean can check mechanically.

This makes formalization a valuable safeguard. If a proof is correctly encoded and the system accepts it, the logical steps in that formal proof have passed the checker.

However, formal verification has limits. Lean does not independently establish that the formalized theorem is the right interpretation of the original research problem. Researchers must still determine whether the assumptions, definitions and conclusion match the intended mathematical claim.

That is why OpenAI’s use of Lean and its decision to involve external experts serve complementary purposes. Formal checking tests the internal logic of the encoded argument; independent review evaluates the mathematics, its interpretation and its wider implications.

What This Means for AI Research and the Scientific Community

The initiative could help establish a more rigorous process for AI-assisted discovery. As models become capable of producing longer technical arguments, researchers will need methods for distinguishing genuinely new results from plausible-looking but incorrect outputs.

The process also raises questions about scientific credit and access. OpenAI says it does not seek academic credit for discoveries generated by its internal models. Instead, it wants the experts who explain the results and develop the supporting research to receive recognition for their contributions.

There is also a transparency challenge. Different release strategies may make some results easier to inspect than others. Publishing a complete proof enables broad scrutiny, while holding back technical materials can allow specialists to produce a more coherent explanation—but limits immediate independent access.

The success of this approach will depend on whether the reviewers can validate the claims, identify limitations and communicate their conclusions openly. The fact that a prominent researcher has agreed to examine a result should not be confused with endorsement of that result.

The Bigger Picture

OpenAI’s announcement points to a potential change in how advanced AI systems contribute to science. Instead of serving only as assistants for literature searches, calculations and routine coding, models may increasingly propose arguments that researchers must evaluate at the frontier of their fields.

That possibility is significant, but it also raises the standard for evidence. A scientific breakthrough is not established simply because an AI produces a paper or a formal proof. Independent scrutiny, reproducibility and expert interpretation remain essential, especially when a claim challenges a foundational assumption or addresses a longstanding open problem.

The three collaborations offer an early test of how that verification process can work. If the proofs survive scrutiny, they could lead to substantial advances in their respective fields. If reviewers find gaps, the work may still provide useful research directions. Either outcome will help clarify how AI-generated discoveries should be assessed and shared.

FAQs

1. What AI breakthroughs has OpenAI announced?

OpenAI says its internal models produced three results: a proof of the local smoothing conjecture in all dimensions, a proposed disproof of the Exponential Time Hypothesis, and an existence proof for certain four-dimensional quantum field theories, including Yang–Mills theory.

2. Has OpenAI’s AI solved P versus NP?

No. Even if the claimed disproof of the Exponential Time Hypothesis is correct, it would not automatically settle P versus NP. These are related but distinct questions in computational complexity theory.

3. Who is checking OpenAI’s AI-generated proofs?

The computer-science result is being examined by Russell Impagliazzo, Ramamohan Paturi and Ryan Williams. The physics collaboration is led by Nobel laureate David Gross and includes Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov. The mathematics proof has been published for researchers to examine.

4. What is Lean, and why is it important?

Lean is a proof assistant that checks formal mathematical arguments against precisely stated definitions and assumptions. It can verify the logical structure of an encoded proof, but experts must still confirm that the formal statement correctly represents the intended research problem.

5. Has OpenAI solved the Yang–Mills Millennium Prize Problem?

Not completely. OpenAI claims an existence proof for pure Yang–Mills theory, but the Millennium Prize Problem also requires proving a mass gap. OpenAI has not claimed to have resolved that additional requirement.

Looking Ahead

The next important development will be the independent researchers’ conclusions. The computer-science group plans to make its examination accessible to the wider community, while the physics group is working toward its own write-up. The mathematics result will depend on researchers independently checking the published proof and formalization.

For the AI industry, the outcome could influence how companies disclose scientific discoveries, provide access to underlying evidence and work with academic researchers. The long-term measure of success will not be how extraordinary an AI-generated claim sounds, but whether independent experts can verify it and turn it into reliable scientific knowledge.