⏱️ Reading time: 9 min
On October 18, 2026, an OpenAI model produced a proof that, according to the company, refutes a computational complexity conjecture that had stood since 1999: the Exponential Time Hypothesis.
📑 En este artículo
The proof was formalized in Lean a day later and is one of three discoveries OpenAI presented on October 26, alongside a new protocol for working with academic communities.
TL;DR
- An OpenAI model refuted the ETH, the complexity assumption in place since 1999 that underpinned hundreds of papers.
- The proof was verified in Lean and published on GitHub on October 26, 2026.
- The same release includes a mathematical proof that solves the Kakeya conjecture in all dimensions.
- OpenAI sets four principles for its academic collaborations: transparency, recognition, and independence.
- For the physics result, the external group decided not to publish the AI-generated materials yet.
What Is the Exponential Time Hypothesis
The Exponential Time Hypothesis is a complexity theory conjecture formulated in 1999 by Russell Impagliazzo and Ramamohan Paturi. It states that no algorithm can solve 3-SAT, the Boolean satisfiability problem with three-literal clauses, in subexponential time in the worst case.
The ETH acronym appears in hundreds of papers on graph theory, databases, computational biology, and computational geometry, which cite it to justify why certain problems admit no fast algorithms. It is a stronger assumption than simply assuming P is different from NP: it sets a concrete exponential floor, not just the absence of a polynomial algorithm.
What Happened
On October 26, 2026, OpenAI announced three results produced by its models: a harmonic analysis proof that also solves the Kakeya conjecture along the way, a refutation of the ETH in complexity theory, and a third result in quantum field theory that the company has not yet detailed publicly. All three went through the same filter before release: an external expert, acting as a “shepherd,” recommended how to present each finding to the relevant academic community, rather than having OpenAI decide alone.
| Area | Publication strategy | What was released |
|---|---|---|
| Mathematics (local smoothing and Kakeya) | Open publication; researchers organize on their own | Natural-language write-up and formal Lean proof, on GitHub |
| Computational complexity (ETH) | An external group explains the result while the model’s output remains public | Natural-language write-up and Lean formalization, on GitHub |
| Physics (quantum field theory) | An external group decides what to release; for now they prefer to write it themselves | Nothing published yet |
OpenAI says it doesn’t yet know which of the three strategies works best and is asking for feedback on how to broaden participation. The process rests on four principles the company set for these collaborations:
- Transparency: the existence of the collaboration is public, and participants are not asked to sign confidentiality agreements.
- No academic credit: OpenAI does not claim academic authorship for findings from its internal models.
- Recognition: the external group receives credit for the work of explaining, writing up, and contextualizing the result.
- Independence: participation is voluntary and unpaid, and each group’s conclusions are its own, not OpenAI’s.
flowchart TD
A["OpenAI model"] --> B["New result: math, complexity, or physics"]
B --> C["An external expert acts as shepherd"]
C --> D["A release strategy is chosen"]
D --> E["Math: open release on GitHub"]
D --> F["Complexity (ETH): group explains, output public"]
D --> G["Physics: group decides, output contained"]Context and History
The ETH did not originate with OpenAI. It was proposed by Russell Impagliazzo and Ramamohan Paturi in 1999 as a finer-grained hypothesis than the open P versus NP question: it sets a concrete exponential floor for the worst case of 3-SAT, not just the absence of a polynomial algorithm. Since then, hundreds of papers in graph theory, databases, computational biology, and computational geometry have used the ETH as a starting assumption to prove that their own problems are also hard, through reductions that inherit the hardness of 3-SAT.
The mathematical result has an equally long parallel history. In 1991, Christopher Sogge proposed the local smoothing conjecture, about how a wave focuses at the worst possible moment versus what happens at a typical instant. That conjecture implies, among other things, the Kakeya conjecture and the Stein restriction conjecture. In 2019, Larry Guth, Hong Wang, and Ruixiang Zhang proved the local smoothing case in two dimensions; in 2025, Hong Wang and Joshua Zahl solved Kakeya in three dimensions. OpenAI’s model, according to the company, proves the local smoothing case in all dimensions and solves Kakeya and Stein’s conjecture along the way for any number of dimensions, relying on a novel auxiliary partial differential equation different from the ones used in earlier proofs.
This is not the first mathematical result OpenAI has released this way: the company says it applied the same open-publication strategy in an announcement on October 6, 2026. The difference this time is that the complexity result did go through a group of external collaborators beforehand.
Technical Details: The Mechanism Behind the Refutation
The Exponential Time Hypothesis does not say 3-SAT is unsolvable: it says any correct algorithm needs exponential time in the worst case, no matter how clever it is. Formally, it states that no algorithm solves 3-SAT in 2^o(n) time, that is, strictly less than exponential in the number of variables n. Refuting it requires showing, even without explicitly constructing it, that such an algorithm exists.
OpenAI did not publicly detail the technique used for the complexity proof: the announcement only confirms that the demonstration was produced by the model and formally verified in Lean. Where there is more detail is in the mathematical result, which the company says relies on a novel auxiliary partial differential equation, different from the harmonic analysis tools Guth, Wang, and Zhang used for the two-dimensional case.
Verification in Lean is what sets this announcement apart from an unsupported claim. A type checker like Lean rejects any invalid logical step, so a successful compilation confirms that the chain of inferences is correct within the declared formal system. That doesn’t eliminate all risk: Lean validates that the proof is internally consistent, not that the way “3-SAT” or “subexponential time” were translated into Lean axioms exactly captures what the complexity community means by those terms. That translation, the formalization of the statement and not just the proof, is precisely what the ETH’s external collaborator group is reviewing before the result is considered confirmed by the community.
📌 Note: Lean accepting a proof confirms it is logically valid within the declared axioms, not that those axioms correctly describe the real problem it set out to solve.
Impact and Analysis
The implications are not automatic. The hundreds of papers that assumed the ETH to prove conditional hardness for their own problems remain logically correct: they showed that if the ETH is true, then their problem is hard. What changes is that this premise, if the refutation withstands scrutiny, is no longer true, so the conclusion is no longer guaranteed. Each of those results will need to be revisited to see whether it still holds under a different assumption, or whether it was actually weaker than it seemed.
The refutation also doesn’t yet deliver a usable algorithm. Showing that a subexponential algorithm for 3-SAT exists is not the same as publishing one with a reasonable constant: many existence proofs in complexity theory are non-constructive or produce algorithms with constants so large they are useless in practice. OpenAI’s own announcement frames this cautiously: the refutation reopens questions about how much faster these tasks could become, but guiding the search for better algorithms is not the same as having finished it.
There is also an asymmetry that OpenAI acknowledges in its own announcement: choosing the first shepherds determines who finds out first and who shapes the initial narrative of each finding. The company says it is open to suggestions on how to broaden that participation, but for now the criteria for selecting those experts are not public.
What’s Next
The computer science collaborator group has already decided to immediately make public the natural-language write-up and the Lean formalization of the ETH result, and both are in OpenAI’s GitHub repository. The work that remains is outside the company: complexity theory specialists need to review the formalization of the statement, not just the proof, and the community needs to start mapping which ETH-conditioned results still hold and which don’t.
For the physics result, on the other hand, there is nothing to review yet: the external group chose to write its own material before publishing the artifacts the model generated. OpenAI gave no date for that publication.
If you want to check it firsthand, the natural-language write-up and the Lean formalization of the ETH result are already published in OpenAI’s GitHub repository, open for anyone to read or try to find an error in them.
Frequently Asked Questions
What is the Exponential Time Hypothesis?
It’s the conjecture, formulated in 1999, that no algorithm solves 3-SAT in subexponential time in the worst case. It serves as the basis for conditional hardness proofs in dozens of problems related to Boolean satisfiability.
Why did the ETH matter so much to complexity theory?
Because hundreds of papers used it as a starting assumption to show that their own problems, in areas like databases or computational biology, are also computationally hard.
What does it mean for 3-SAT algorithms if the ETH is false?
In principle, it implies that an algorithm capable of solving 3-SAT in subexponential time exists, although the proof doesn’t explicitly construct it or say whether it would be useful in practice.
What is the Kakeya conjecture that OpenAI’s model also solved?
It’s a geometry problem about the minimum size a set must have if it contains line segments in every possible direction; it was solved in three dimensions in 2025, and now, according to OpenAI, in all dimensions.
Where can you review OpenAI’s Lean proof?
The natural-language write-up and the Lean formalization of the ETH result are published in OpenAI’s GitHub repository, available for anyone who wants to audit them.
References
- OpenAI: official announcement of the three discoveries and the new academic collaboration protocol.
- Wikipedia: definition and origin of the Exponential Time Hypothesis.
- Wikipedia: explanation of the Kakeya conjecture.
- Wikipedia: context on the P versus NP problem.
- GitHub: OpenAI’s repository where the proofs and Lean formalizations are published.
📱 Do you like this content? Follow @programacion on Telegram for daily tech content in Spanish: quick summaries, fresh content every day.
Featured image: Foto de Conny Schneider en Unsplash
Did it work for you? Got a different error? Say so below: questions get answered and help the next reader.
Leave a comment
0 Comments