Fedor Fomin, a computer scientist at the University of Bergen in Norway, had written a textbook on the subject he has spent his career on. He now expects it to be obsolete.
The occasion was a blog post OpenAI published on Oct. 26, announcing that its internal models had produced three results: one in harmonic analysis, one in complexity theory and one in quantum field theory. The computer science result, if it holds, refutes the Exponential Time Hypothesis, an assumption proposed nearly 30 years ago about how quickly certain logical problems can be solved. “This came as a complete surprise, a shock,” Fomin said. “Nobody I know expected it.”
The Exponential Time Hypothesis concerns satisfiability, the problem of deciding whether a logical formula whose variables can only be true or false can be made true. Checking an answer is easy; finding one is not, because every added variable doubles the number of combinations. The hypothesis says no shortcut changes that: worst-case computing time keeps growing exponentially with the size of the problem.
OpenAI says its models found an algorithm that beats the assumed limit, which would make the hypothesis false. Leslie Goldberg of the University of Oxford said that, assuming confirmation, the result is an enormous breakthrough, and that it would require a complete revision of several areas of algorithms and complexity. He also drew a boundary that the headlines missed: the hypothesis sits near the P versus NP question, but refuting one does not settle the other.
The other two results arrive with similar caveats. In mathematics, OpenAI says the models proved a 1991 conjecture that waves cannot stay sharply focused for long, a result that bears on how thin a shape can be while still containing line segments pointing in every direction. In physics, the company says the models proved that quantum field theories, including quantum chromodynamics, are mathematically well defined rather than merely predictive. That touches the existence of pure Yang-Mills theory, one of the Millennium Prize problems, without resolving it.
Verification is now the whole question, and OpenAI has structured the release around that rather than around the claims. The company described the manuscripts as a form of raw research data, and asked outside experts to act as shepherds who organize groups to understand them. The experts advised three different approaches, and OpenAI used all three.
For the mathematics result, the model output is being published as is, leaving researchers to organize the work of explaining it. For the computer science result, an external group will explain it while the material is released publicly, and the natural-language proof and its Lean formalization went to a public repository immediately. For the physics result, the external collaborators will write it up themselves and have held back the model-produced artifacts for now.
Lean is a programming language in which a proof can be checked step by step by a machine. It rules out arithmetic slips and gaps in reasoning, and it does not rule out the more common failure, which is a formal statement that does not capture the problem a mathematician meant to solve. A proof that verifies in Lean can still be a proof of the wrong theorem.
OpenAI set four conditions for the collaborations. Participants do not sign nondisclosure agreements and may discuss the work, share intermediate results and publish conclusions. OpenAI does not seek academic credit for discoveries made by its internal models, and says that inviting a researcher to shepherd a collaboration does not imply that the researcher made the discovery. The groups get credit for the understanding they produce. Participation is voluntary and unpaid, and members’ conclusions are their own.
That last set of terms is unusually specific for a corporate research announcement, and it reads like an answer to a criticism. Mathematicians have spent two years arguing about what it means when a machine produces a result that no human can explain, and about who is accountable when the result turns out to be wrong. The arrangement OpenAI describes transfers the explaining, and with it the accountability, to people who are not employed by OpenAI and are free to say the proofs are flawed.
The timing adds pressure. Less than a month ago the company published several hundred mathematical manuscripts that are still being reviewed by outside researchers, and this batch will face the same process, with the addition of a formal verification step that has never been applied at this scale to results produced this way. Publication is the beginning of the review, not the end of it.
For the field, the practical consequence is a queue. Journals that have no procedure for machine-generated proofs will need one. Referees who would ordinarily spend months on a single paper will be asked to triage work that arrives faster than it can be read. Textbooks that rest on the Exponential Time Hypothesis, including the one Fomin wrote, will sit in a state of suspension until someone confirms or finds the error.
For OpenAI, the value is not the credit it declines. It is the demonstration that a model can produce work at the frontier of fields where progress is measured in decades, at a moment when the company is arguing to investors and regulators that its systems are worth their cost. Whether the three proofs stand is now a question for the people who were handed them.
