OpenAI says its internal models refuted the Exponential Time Hypothesis and proved the Kakeya conjecture in every dimension

On October 26, OpenAI published three results that it says unreleased internal models produced. The results concern problems in theoretical computer science, harmonic analysis and mathematical physics that specialists have worked on for decades. The company also explained how outside researchers can check the work. All three are claims, and none has been independently confirmed yet.

The computer science result is the sharpest. A preprint dated October 25 describes a deterministic algorithm that exactly counts the satisfying assignments of k-CNF formulas with fixed clause width, running in subexponential time using polynomial space, according to coverage of the paper. The Exponential Time Hypothesis (ETH) holds that 3-SAT requires time of 2 to the power of some constant times n. Any subexponential bound for this problem would refute it. OpenAI says it found the natural-language argument on October 16 and formalized it in Lean the next day.

The mathematics claim is a proof, in every dimension, of the local smoothing conjecture that Christopher Sogge proposed in 1991. That result would also settle the Kakeya and Stein restriction conjectures in all dimensions, The Next Web reported. Local smoothing had previously been proved only in two dimensions, a result from 2019, and Hong Wang and Joshua Zahl proved the three-dimensional Kakeya case in 2025. A summary of the announcement from a Russian-language research channel describes local smoothing as a bound on how strongly waves can concentrate. The physics claim is a rigorous existence proof for four-dimensional quantum field theories, including quantum chromodynamics, according to Unite.AI.

Russell Impagliazzo and Ramamohan Paturi of UC San Diego and Ryan Williams of MIT are organizing the review of the ETH claim. Impagliazzo and Paturi co-authored the original hypothesis. Williams called the work "a claimed refutation of ETH" and said the review group has signed no nondisclosure agreements and will receive no compensation. A Lean check confirms that a proof establishes its encoded statement, but it does not confirm that the formal definitions match the intended conjecture, and reviewers have flagged that gap.

OpenAI's recent record calls for caution. On October 6 it released 722 manuscripts in 372 result families. It withdrew three of them the next day, after a sign error invalidated one result and, through dependencies, two others that relied on it. The repository states that 42% of top-line results are Lean-formalized, but independent recounts put the share at 24% to 36%. Scientific American reported widespread skepticism among mathematicians. Terence Tao has raised concerns about results claimed by people who may not understand the proofs well enough to defend them, and Tristan Buckmaster has asked whether some results complete unpublished human work.

Even if it holds, the ETH result has no near-term practical effect. The bound is superpolynomial, so the P versus NP question is untouched, and the crossover point below 2 to the n lies far beyond any formula size anyone will ever actually solve. SAT solvers and deployed cryptography are unaffected. The effect would fall on fine-grained complexity theory, where many conditional lower bounds assume ETH. OpenAI made the announcement the same day Anthropic filed to go public, and a lab competing for the same investor capital gains from putting out a capability claim on that date.