OpenAI releases two AI-made proofs as scientists debate how to verify a third

The story

OpenAI has announced three sweeping AI-generated research claims spanning mathematics, theoretical computer science and physics, while testing three different ways to let outside scientists examine them. The company released natural-language and Lean proof packages for two claims on October 26. It has not released the underlying materials for the third, a decision that immediately drew a public objection from an independent mathematics advisory group. None of the three claims should yet be treated as a settled scientific result.

The mathematics result concerns local smoothing for the Euclidean wave equation. Proposed by Christopher Sogge in 1991, the conjecture describes how sharply waves can remain concentrated after their behavior is averaged over time. OpenAI says its internal model produced a proof in every spatial dimension of at least two, using a new auxiliary partial differential equation. If the argument survives scrutiny, the company says it would also resolve the Kakeya and Stein restriction conjectures across their stated ranges. The natural-language output and a Lean formalization are public on GitHub.

That scope matters. Previous work proved local smoothing in two dimensions, while Hong Wang and Joshua Zahl resolved the three-dimensional Kakeya conjecture in 2025. OpenAI says its output arrived on October 18 and was formalized the next day. But a machine-checked proof is not a one-click certificate for the full headline. Reviewers must confirm that the formal statement faithfully represents the claimed theorem, that every imported assumption is appropriate, and that the argument is genuinely new rather than an unrecognized reformulation of prior work.

The computer-science claim is potentially broader. The Exponential Time Hypothesis, or ETH, has long been used to argue that many computational problems cannot be solved substantially faster than exhaustive search in the worst case. OpenAI says its system found a deterministic, subexponential-time algorithm for exactly counting satisfying assignments of fixed-width Boolean formulas, with the 3-SAT case refuting ETH. It released both the prose proof and Lean code after consulting a group led by UC San Diego researchers Russell Impagliazzo and Ramamohan Paturi, who helped formulate ETH, and MIT computer scientist Ryan Williams.

A valid refutation would force complexity theorists to revisit hundreds of conditional hardness results. It would not automatically make today’s industrial optimization or security problems easy. Asymptotic improvements can be impractical at realistic input sizes, and ETH is distinct from the larger P-versus-NP question. The immediate task is therefore narrower: reconstruct the algorithm, test the formalization’s correspondence to the paper and identify which downstream theorems truly depend on the version of ETH being challenged.

The physics claim is the hardest to evaluate because its evidence is not yet public. OpenAI describes a rigorous existence proof for certain four-dimensional interacting quantum field theories containing gauge fields and fermions, including quantum chromodynamics and a unified completion of the Standard Model. It says the work includes pure Yang–Mills theory as a subproblem. Nobel laureate David Gross is leading a group with Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov to understand and write up the result before deciding how the artifacts should be released.

That controlled approach has become part of the story. OpenAI says external participants are unpaid, independent, free to discuss the work and not being asked to endorse the company. It also acknowledges that selecting initial reviewers creates unequal access. The independent Advisory Group on Mathematics and Artificial Intelligence went further on October 26, calling for immediate publication of the Yang–Mills, QCD and Standard Model outputs. The group argues that designated experts can receive a head start, discourage broader participation and lend their reputations to claims before community review.

The disagreement exposes a new bottleneck in AI-assisted science. A laboratory can generate manuscripts and formal artifacts faster than specialist communities can read, contextualize and challenge them. Immediate release maximizes equal access but can transfer the cost of explanation and error-finding to researchers. Staged review may improve exposition, yet it concentrates information and lets a company shape who first interprets work that could redirect entire fields. Neither route substitutes for a durable scholarly record, explicit model and compute disclosures, careful citations and independent reproduction.

INNOVOX analysis: the consequential development is not that an AI laboratory has declared three problems solved. It is that AI-generated research is forcing science to design a verification system at the same time as it assesses the results. Lean can expose logical gaps inside a formal statement; expert review can test whether that statement answers the problem scientists care about; open publication can reveal missing citations and competing claims. Credibility requires all three layers, with clear separation between company assertions and independently established knowledge.

What to watch next is evidence, not scale. For local smoothing and ETH, specialists need to produce readable reconstructions, check the code against the prose and map the consequences without inflating them. For the physics claim, the underlying files and exact theorem statements must become public before outsiders can assess them. If those steps confirm even one result, the scientific importance could be substantial. Until then, the release is best understood as a set of unusually serious claims accompanied by an unfinished experiment in how machine-generated discovery should enter human science.

INNOVOX analysis

The most important innovation may be the verification pipeline rather than any single theorem. AI systems can now generate research faster than specialist communities can contextualize it, creating a need for public artifacts, reproducible formal checks, transparent problem selection and credit for the human work that turns machine output into durable knowledge.

What to watch

Watch for independent reconstructions of the two released proofs, publication of the physics artifacts, and precise statements about what the Yang–Mills work establishes. The strongest signal will be experts reproducing the arguments and identifying genuinely new methods—not additional headline claims.