Based on OpenAI's public announcements of October 26, 2026 and cross-checked reporting | Information current as of the evening of October 27
On October 26, OpenAI announced in one burst three results produced by an internal research model: a proof of the local smoothing conjecture in all dimensions (harmonic analysis), a refutation of the Exponential Time Hypothesis (computational complexity theory), and a rigorous mathematical existence proof for four-dimensional Yang-Mills theory (quantum field theory). Reactions stretched to both ends of the opinion spectrum: on one side, the social-network cheer that "if these hold up, this is the biggest single day in the history of math and theoretical computer science"; on the other, the demand to "put the AI back in its cage." Both are right, because the most revealing part of this event is not the three proofs themselves but the three different trust tiers OpenAI assigned to them.
1. Three Announcements, Three Levels of Trust
Start with the facts. All three claims come from an unreleased internal research model. For the computer science result, the model produced a natural-language proof on October 16 and completed Lean formal verification the next day: one day from proof to machine-checked, line by line.
But OpenAI adopted three markedly different release strategies for the three results, and this detail says more than the results themselves:
| Claim | Released materials | Vetting arrangement |
|---|---|---|
| ETH refuted | 67-page paper + Lean 4 code, fully public | Original proposers Impagliazzo and Paturi, with MIT's Ryan Williams, organize an open independent review |
| Local smoothing conjecture (all dimensions) | 59-page paper + Lean 4 code, fully public | Experts advised direct release, for researchers to work through on their own |
| Yang-Mills existence, 4D | Preprint and code not released | Handed to five physicists, including Arthur Jaffe and David Gross, to rewrite and digest first |
The first tier is "everything released, reviewed by the original proposers": Russell Impagliazzo and Ramamohan Paturi, who defined the hypothesis in 1999, have been invited to examine whether AI overturned it, alongside the review's third member, MIT's Ryan Williams, a leading scholar in lower bounds and algorithm design. The three have stated explicitly that organizing the review does not amount to endorsing the result. OpenAI has also agreed to fund a conference organizing the global academic community's examination.
The second tier is "everything released, community digests": for the mathematics direction, the advising experts recommended simply publishing the AI-generated manuscripts and letting researchers derive and refine them. In OpenAI's own words, the most appropriate way to read these manuscripts is as "raw research data," not as papers.
The third tier is "nothing released, authorities rewrite first": although OpenAI says the Yang-Mills work passed formal verification on October 16, it is the only one of the three with no manuscript posted. The stated reason is that five physicists are rewriting and digesting it first.
Three strategies, three self-assessed credibility levels. This may be the first time an AI lab has admitted so plainly that AI-generated proofs do not all deserve the same trust.
2. ETH: The Pillar Under Thirty Years of Lower Bounds
The result that genuinely stunned theoretical computer science is the ETH refutation. To understand it, start with a combination lock: n dials, each set to 0 or 1. You do not know the password, but you hold a stack of clues, each involving at most three dials—"dials one and two cannot both be 0," "dial two is 0, or dial three is 0." Is there an assignment satisfying every clue? This is 3-SAT, the patriarch of NP-complete problems.
A four-dial lock has at most 16 combinations. A hundred-dial lock has 2^100; a clever algorithm need not try them all, but for general 3-SAT, how fast can an algorithm possibly be? In 1999, Impagliazzo and Paturi gave their answer: no algorithm running in 2^{o(n)} time (subexponential) solves general 3-SAT; in the worst case, exponential cost in the number of variables cannot be avoided. This is the Exponential Time Hypothesis.
The hypothesis was never proved, but for nearly thirty years almost everyone believed it, and on top of it they built an entire edifice of conditional lower bounds: hundreds of papers in graph theory, database queries, computational geometry, and computational biology whose conclusions read "assuming ETH, problem X admits no subquadratic-time algorithm." ETH became the coordinate origin for declaring "computational death sentences" in theoretical computer science.
OpenAI's paper title is unambiguous: "The Exponential Time Hypothesis Is False." The manuscript gives a deterministic algorithm that, in subexponential time exp(n/(log n)^{1/2+o(1)}) and polynomial space, exactly counts the number of satisfying assignments of constant-width CNF formulas. Note that this is the counting version: not merely deciding whether a solution exists, but counting solutions exactly, which is stronger than decision. 3-SAT is a special case. If a subexponential algorithm exists, ETH's assertion is negated.
Three boundaries must be drawn. First, this does not prove P=NP: ETH implies P≠NP, so conversely, a refutation of ETH only shows that 3-SAT has a subexponential algorithm, still an essential distance from polynomial time. The door between P and NP has not opened. Second, cryptography is not broken today: subexponential still means astronomically large; on the order of exp(n/√log n), the workload at n=1000 runs to roughly 10^95–10^165 depending on the logarithm base, with no engineering significance. Third, this algorithm will not ship in any practical SAT solver: its value is not speed, but erasing a meridian from the lower-bound map.
What about the hundreds of papers built on ETH? Logically they remain valid—"if ETH then X" is still a theorem. But the plausibility of the premise has collapsed, and the practical meaning of those bounds needs reassessment: either find unconditional proofs, or substitute an assumption that is still believable. And since the stronger SETH (Strong Exponential Time Hypothesis) implies ETH, ETH's fall also pulls the premise out from under the lower bounds conditional on SETH. Rarely in the history of science has this happened: the people who posed the question have been invited back to organize the review of an AI proof that overturns their own hypothesis.
3. Kakeya and Yang-Mills: The Other Two Claims
The mathematics result carries real weight as well. The local smoothing conjecture is a central problem in harmonic analysis, concerning how the regularity of solutions to the wave equation evolves in time; it implies the Kakeya maximal conjecture, the Kakeya dimension conjecture, and Stein's spherical restriction estimate—together, it nearly levels four classic open problems in the field. The background deserves respect: in February 2025, Hong Wang and Joshua Zahl settled the three-dimensional Kakeya conjecture in a paper of over a hundred pages, an achievement hailed as a once-in-a-generation advance in harmonic analysis. OpenAI now claims local smoothing in all dimensions (n≥2), a broader sweep, and reportedly the core tool is an auxiliary partial differential equation nobody had used before—if it holds, this is a toolbox-level upgrade, not a single-point breakthrough. The 59-page preprint and Lean 4 code are fully public.
The physics claim warrants far more restraint. The Clay Millennium problem "Yang-Mills Existence and Mass Gap" asks for two things: constructive existence, meaning the rigorous construction of a nontrivial quantum gauge theory in four dimensions satisfying the axioms (Wightman or Osterwalder-Schrader reflection positivity), and a proof of the mass gap. OpenAI's claim concerns the first: existence for four-dimensional QCD and pure Yang-Mills. The mass gap is not mentioned. Quantum field theory, the foundation of modern physics, has never had a rigorous mathematical footing; any real progress is significant. But this is the one claim of the three with no published manuscript or code, and the loudest community discussion is precisely about that contrast: why does a result that reportedly passed formal verification on October 16 come with no original materials? The official account is that five physicists—including the problem's author Arthur Jaffe and Nobel laureate David Gross—are rewriting it first. That arrangement is defensible; the translation between physics-style proofs and traditional mathematical formalization may be enormous. But it also means this claim currently rests entirely on the credibility of five experts, with no entry point for outsiders to check.
4. What Lean Verification Can and Cannot Prove
The "formal verification in one day" narrative needs a precise decomposition, because it sits at the exact intersection of all the excitement and all the controversy.
What a proof assistant like Lean does: given a formal statement and a proof script, the machine checks, line by line, that every inference step follows from axioms and previously established theorems. What it proves is: if the statement is the right one, the proof has no gaps. On this, machines beat humans—human reviewers get tired, skip steps, and are persuaded by fame; Lean is not.
What it cannot prove: whether the statement faithfully captures the mathematical proposition you meant. Translating "ETH is false" into a formal language involves choices: how each definition maps, how quantifiers are ordered, how boundary conditions are handled. Those translation steps still come from humans (or AI). A Lean-verified script can perfectly well prove a proposition subtly different from the intended one—incidents of this "statement correctness" kind are not unheard of in the formalization community. That is exactly why the review group of Impagliazzo, Paturi, and Williams remains necessary: the machine owns the inference chain; people own the statement and its meaning.
This also explains why OpenAI's "raw research data" framing is smart. Three weeks earlier (October 6), OpenAI had released 722 AI-generated mathematical manuscripts (372 result families, 17 directions), and Nature's headline at the time was "the verification crisis of AI mathematics." The three announcements are the post-mortem edition: no longer throwing AI manuscripts out as papers, but processing them in tiers—formalize what can be formalized, organize reviews where review is possible, and let authorities digest first where translation costs are enormous. The release process itself became part of the research output.
One observation about the information ecosystem: a claim has circulated in Chinese-language coverage that Anthropic's Claude independently found a similar ETH refutation the same day, "independent and concurrent." As of this writing, it traces to a single Chinese source, with no Anthropic statement or second source. It is a fitting specimen of this week's information ecology: the more a rumor fits the "AI race" narrative, the faster it travels and the costlier it is to check.
5. Reactions and Points of Contention
The reaction spectrum stretches wide. Nobel laureate David Gross said that for anyone outside the field, ETH being refuted is "very surprising, and the implications are far-reaching." Tsinghua complexity theorist Lijie Chen publicly reflected on "the Exponential Time Hypothesis being false." On social networks, one model-generated reflection called it "the biggest single day in the history of mathematics and theoretical computer science, if it holds," while a sizable chorus demanded AI be "put back in its cage." Terence Tao had earlier shared a statement from the "Association for Human Mathematics" responding to the 722 manuscripts, representing the mathematical community's institutional wariness of the flood of AI papers.
The contention concentrates on four points.
The dispute over the research model. "Raw research data" implies a complete division of labor: AI produces proofs; human mathematicians translate, explain, and digest. Supporters call it leverage for mathematicians; skeptics ask: if comprehension cannot keep pace with production, is mathematical knowledge still human knowledge? What is the epistemic status of a proof nobody understands?
The cascade review of conditional results. Hundreds of "assuming ETH" lower-bound papers face a reassessment of their premise. This is textbook-revision-scale work, and it may also seed a wave of papers rebuilding bounds under new assumptions—for the theory community, both a loss and a subject bonanza.
The polarization of media narratives. Coverage swung between celebratory framing—AI cracking three century-old problems overnight—and sober reminders that independent verification has not happened, in sharp contrast to the reviewers' restraint of "participation is not endorsement." The key to a cold reading: everything so far is "OpenAI's claim plus machine verification passed." The independent human review has just begun, and cases do exist in the history of formalization where verified proofs later turned out to prove the wrong statement.
The gap between theory and engineering. A subexponential algorithm has no engineering significance for n=1000 instances and will not change the running speed of any deployed system in the near term. ETH's fall redraws the theoretical map of what is possible, not the practical map of what is feasible. Conflating the two is the most common amplifier of this kind of news.
6. How to Read This Event
Three judgments.
First, the gradation of credibility matters more than the conclusions themselves. The three claims shipped with three release strategies—the first time AI scientific output has been institutionally treated as an object of tiered trust. Whatever the fate of the three proofs, the three-layer structure of "AI proof + Lean verification + human review of statements" is likely to become the standard pipeline for AI research output going forward.
Second, the asymmetry of verification is the real news. AI-written marketing copy cannot be machine-checked; AI-written proofs can. Fields that can be formalized—mathematics, theoretical computer science, parts of theoretical physics—will feel the impact of AI production first, because machine checking radically lowers the cost of trust; fields that cannot be formalized still depend on traditional peer review. The order in which disciplines benefit from AI is being re-sorted by verifiability.
Third, it is too early to conclude that "AI leads humanity in understanding the universe." The ETH review has not concluded, the Yang-Mills manuscript has not been released, and the local smoothing proof awaits community digestion. What may be remembered is the image: the people who proposed the hypothesis in 1999 organizing, in 2026, the review of an AI proof that overturns it. The scientific community's self-correcting mechanism is being activated by this shock, not disabled.
Four things to watch: the review group's public conclusion on the ETH proof; independent recomputation of the Lean code (anyone can run it); whether the Yang-Mills manuscript is released; and how the wave of conditional lower-bound reassessment unfolds. Until the independent review lands, every statement in this article that "ETH has been refuted" should be read as "OpenAI claims, machine verification passed, human review in progress."
Sources
- OpenAI public announcement of 2026-10-26 and its GitHub repository (67-page ETH paper, 59-page local smoothing paper, Lean 4 code)
- JiQiZhiXin (machine heart), "OpenAI Topples a 30-Year Cornerstone of Computer Science, and Solves the Kakeya Conjecture" (2026-10-27)
- XinZhiYuan, "'The King's Conjecture' Falls in All Dimensions; the 30-Year Iron Law of ETH Collapses" (2026-10-27)
- 51CTO, "OpenAI Announces Solutions to Three Century-Old Scientific Problems" (2026-10-27)
- NetEase (review-arrangement details; its claim of a concurrent Anthropic replication is single-source and not adopted as fact)
- Zhihu Q&A threads: breakdown of the Yang-Mills existence problem statement; discussion of the local smoothing release process (2026-10-27)
- Techmeme front page, 2026-10-27 (English-language reaction spectrum)
- Hong Wang and Joshua Zahl, proof of the three-dimensional Kakeya conjecture (2025-02, arXiv)
This article is research analysis. The final validity of the three claims rests with the conclusions of independent academic review.