OpenAI says its models produced proofs overturning a complexity cornerstone

Key Points

1. OpenAI announced three results on October 26 it says internal models generated, each with a different release strategy.
2. One claims the Exponential Time Hypothesis, used in hundreds of papers, is false; another covers Yang-Mills existence.
3. If academics validate the work, models shift from research assistants to producers of foundational proofs.

The latest:

Three mathematics, computer science and physics results that OpenAI says were generated by unnamed internal models were published on October 26, each accompanied by a formalization in the Lean proof language. The company described the generated manuscripts as raw research data that still has to be turned into scientific understanding, and said it is testing three different release strategies without yet knowing which works best.

Details:

• The complexity claim: OpenAI said a model produced a proof that the Exponential Time Hypothesis is false, written in natural language on October 16 and formalized in Lean on October 17. The formalization shows that for fixed k ≥ 2 a deterministic machine can count satisfying assignments of a canonically encoded k-CNF formula in sub-exponential time and polynomial space.
• Why ETH matters: The hypothesis has been used in hundreds of papers as a baseline assumption for proving problems hard. Tighter bounds for cases with m clauses appear in a manuscript dated October 25. OpenAI said translating the theoretical progress into practical improvements requires substantial further research.
• Who is checking it: The supervising group is led by Russell Impagliazzo and Ramamohan Paturi of UC San Diego, who proposed the hypothesis with Francis Zane, alongside Ryan Williams of MIT, who refuted strong forms of it. The group asked OpenAI to release all raw data and fund a conference on the work’s implications.
• The mathematics result: OpenAI said a model proved the local smoothing conjecture, posed by Sogge in 1991, in all dimensions using an auxiliary partial differential equation the company called “of a novel kind.” The company said the result also settles the Kakeya conjecture and the Stein restriction conjecture in all dimensions.
• How it was released: The mathematics outputs were produced on October 18, formalized in Lean on October 19, and posted to GitHub with a natural-language explanation, following an earlier October 6 mathematics release. An unnamed outside expert recommended publishing the model outputs directly; no supervising group was named.
• The physics result: OpenAI said a model produced a rigorous existence proof for interacting quantum field theories with gauge fields and fermions in four dimensions, covering quantum chromodynamics and a unified completion of the Standard Model, built on Balaban’s constructive approach. It includes an existence proof for pure Yang-Mills, a sub-problem of the Clay Millennium Prize problems.
• The physics timeline: The Yang-Mills proof was generated in natural language on September 9 and the QCD proof on September 18, with the Yang-Mills Lean formalization completed on October 16; release was held until then. The group is led by Nobel laureate David Gross with Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov.
• The third strategy: The physics group chose to write up the result itself rather than publish model outputs, and asked that correspondence go to a dedicated email address. The computer science group invited the wider community to help organize an open examination of the ETH claim.
• The collaboration terms: OpenAI set four principles: transparency with no confidentiality agreements and participants free to publish; no academic credit for OpenAI and no original-discoverer status from supervising the work; recognition for each group’s own writing; and independence, with unpaid voluntary participation.
• The access gap: The company acknowledged unequal access, saying its choice of initial supervisors determines who participates first, and invited feedback on widening participation. It said it will hand relevant materials and outputs to the groups, and that its 5 million dollar contribution to the Simons Foundation complements the effort.

Background:

The Exponential Time Hypothesis has served as a standard hardness assumption across algorithm design since Impagliazzo and Paturi proposed it with Zane. Yang-Mills existence sits inside the Clay Millennium Prize problem set, among the most prominent open questions in mathematical physics.

Between the lines:

The three different release strategies are the experiment. OpenAI published raw model outputs in mathematics on an outside expert’s advice, handed the ETH claim to the very researchers who proposed the hypothesis, and let the physics group author its own write-up. Each path tests how much verification burden the academic community will absorb, and the company said it does not yet know which works best.

What’s next

Watch for the open examination of the ETH claim the UC San Diego and MIT group invited, the conference OpenAI was asked to fund, and whether the physics group’s own write-up of the Yang-Mills result appears.