OpenAI Says Its AI Broke Three Scientific Barriers. Verification Has Just Begun

OpenAI says its internal AI systems have produced three major theoretical results: a proof of the local smoothing conjecture across all spatial dimensions, an algorithm that would make the widely used Exponential Time Hypothesis false, and a rigorous construction of interacting four-dimensional quantum field theories. The claims are unusually important, but they are not yet three settled discoveries.

Three claims, three release paths

The first result concerns local smoothing, a 1991 conjecture about how sharply waves can concentrate after their behavior is averaged over time. OpenAI says its model produced a proof in every spatial dimension of at least two, extending the two-dimensional result proved in 2019. The company says the argument also resolves versions of the Kakeya and restriction conjectures in higher dimensions.

The second claim targets the Exponential Time Hypothesis, or ETH. Computer scientists have long used ETH as a foundation for conditional statements about how difficult many computational problems are. OpenAI’s manuscript proposes a deterministic, subexponential-time algorithm for exactly counting solutions to fixed-width Boolean formulas. If correct, the case covering 3-SAT would refute ETH.

Key fact: OpenAI published natural-language manuscripts and Lean formalizations for the mathematics and computer-science claims, but withheld the physics artifacts while an external group prepares its own account.

The third claim is the broadest. OpenAI says its model constructed interacting quantum field theories with gauge fields and fermions in four dimensions, including quantum chromodynamics and a unified completion of the Standard Model. A group led by Nobel laureate David Gross is examining the work. Because the underlying AI output is not public, outside researchers cannot yet inspect this claim on equal terms.

What Lean verification does and does not prove

Lean is a proof assistant. Researchers translate definitions, assumptions and logical steps into a formal language, then its kernel checks whether every step follows from the accepted rules. OpenAI’s public note says the ETH formalization verifies an exact counting algorithm for fixed-width formulas within a subexponential time bound.

That is stronger evidence than an unchecked natural-language manuscript, but it is not the end of review. Experts still need to confirm that the formal theorem captures the community’s intended ETH statement, that hidden assumptions are acceptable, that the complexity accounting is sound and that the natural-language conclusions do not exceed what Lean checked. Formal verification also says nothing by itself about whether the ideas are new or properly attributed.

Why the release process is part of the story

OpenAI describes the manuscripts as raw research data rather than finished scientific understanding. It chose different processes after consulting researchers: public release for the local-smoothing proof, a named working group plus public artifacts for ETH, and restricted early access for the physics result.

The company says collaborators are unpaid, may speak freely and will receive credit for explanations and verification rather than for the original AI output. Yet OpenAI also acknowledges that selecting the first reviewers creates unequal access and shapes who can respond first. The Advisory Group on Mathematics and Artificial Intelligence has warned that privileged release can borrow researchers’ reputations before a result is understood.

NewTqnia previously covered OpenAI’s AI-generated Navier-Stokes proof and its unresolved verification and provenance questions. An earlier case showed how AI helped produce a new construction for an Erdős problem without solving the whole question. The new release is broader, but it raises the same distinction between generating a candidate proof and converting it into accepted knowledge.

What happens next

The ETH group, led by Russell Impagliazzo, Ramamohan Paturi and Ryan Williams, plans to examine and explain the algorithm publicly. Separate mathematicians can download the local-smoothing manuscript and formal proof immediately. The physics group will decide when and how to release its account.

The decisive milestone is not another company announcement. It is whether independent specialists can state precisely what was proved, reproduce the formal checks, identify any dependencies or errors and explain why the results change their fields.