OpenAI Says Its AI Disproved a Major Computing Hypothesis

OpenAI says one of its internal AI systems has produced a result that could overturn a long-standing assumption in computer science. In a research announcement published on 26 October, the company said its model had disproved the Exponential Time Hypothesis, or ETH. It also announced proposed breakthroughs in mathematics and theoretical physics. These are unusually consequential claims, but they remain claims to be examined by the researchers who understand the problems best.

ETH is a conjecture about how quickly a computer can solve certain hard problems as their size grows. It concerns Boolean satisfiability, commonly shortened to SAT, which asks whether a set of logical conditions can all be satisfied at once. Researchers have used ETH for decades to establish conditional limits on the speed of algorithms in areas ranging from graph theory to databases. If the proposed refutation survives scrutiny, some of those limits would need to be revisited.

OpenAI says its AI system found a natural-language disproof on 16 October and that the result was subsequently formalised in Lean, software used to check mathematical proofs. The company has published the written manuscript and documentation of the Lean formalisation for others to inspect. The manuscript proposes a subexponential algorithm for counting solutions to fixed-width Boolean formulas. That would be enough to challenge ETH’s assertion about the time required in the worst case.

A faster theoretical bound is not the same thing as a useful new app or an immediate speed boost for today’s computers. Nor does a refutation of ETH automatically resolve the separate P versus NP question or break commonly used encryption. The significance would lie in changing a basic assumption on which many conditional research results depend. Turning a proof into practical algorithms would be another undertaking altogether.

OpenAI says an independent group led by Russell Impagliazzo and Ramamohan Paturi of the University of California San Diego, and Ryan Williams of MIT, will examine and explain the work. Impagliazzo and Paturi helped formulate ETH with Francis Zane. Their participation should not be mistaken for a stamp of approval. The group is organising scrutiny of a potentially important claim, not announcing that the field has accepted it. OpenAI says it agreed to release raw material for examination and fund a conference on the implications.

The mathematical claim concerns the local smoothing conjecture, a question about how waves concentrate over time. OpenAI says its models produced a proof in every dimension, with implications for the Kakeya conjecture and Stein’s restriction conjecture. The company has released both the model’s write-up and a Lean proof description. This follows its earlier release of AI-generated mathematics for public examination, which TechBooky covered earlier this month.

The physics claim is different both in subject and in how it is being released. OpenAI says its models developed a mathematically rigorous existence proof for certain interacting quantum field theories in four dimensions, including quantum chromodynamics, which describes the strong force. The work also includes a proposed proof concerning pure Yang-Mills theory, part of a Clay Mathematics Institute Millennium Prize problem. The company says a group led by Nobel laureate David Gross is examining the material and has chosen not to release the AI-generated artefacts yet. That means outsiders cannot assess this physics claim from the underlying materials in the same way they can examine the published ETH and local smoothing work.

A Lean formalisation can check whether a formal statement follows from the assumptions encoded in it. It does not, by itself, settle whether the encoded statement precisely matches the original research question, whether earlier work has been credited or how much scientific understanding the proof provides. Those are tasks for specialists. OpenAI itself describes the manuscripts as raw research data that must be turned into scientific understanding through academic collaboration.

That caution matters because the company has already faced intense debate over the release and attribution of AI-generated mathematical results. TechBooky previously reported on OpenAI’s independent mathematics advisory group and the questions raised by mathematicians over an earlier prize-problem claim. The new announcement is more than a demonstration of a model answering difficult questions. It tests whether AI labs can put extraordinary findings into the open while giving independent researchers the time, material and credit needed to determine what actually holds up.