OpenAI 请外部专家核查 AI 在数学、计算机科学与物理领域产出的证明

So OpenAI asked outside experts to act as "shepherds" for the results. Based on their advice, the company is handling each field differently. OpenAI says it also translated the math and computer science proofs into Lean.

Lean is a programming language that lets a computer check every step of a proof. That doesn't guarantee the result is error-free, though. Lean only checks whether the proof establishes the statement as it was written in Lean. Experts still have to decide whether that statement actually captures the intended problem.

If OpenAI is right, a core assumption in computer science is wrong

The computer science result centers on the Exponential Time Hypothesis (ETH). It concerns the Boolean satisfiability problem, or SAT. SAT deals with a logical formula whose variables can only be true or false. The question is whether you can set the variables so the whole formula comes out true.

With only a few variables, you can just try every combination. But each new variable doubles the number of possibilities. With 100 variables, you're already looking at a 31-digit number.

Put simply, the ETH says there's no real shortcut. You can speed up the trial and error, but in the worst case, computing time still grows exponentially, increasing by a fixed factor with every added variable.

OpenAI says the satisfiability problem is closely tied to the P versus NP problem. That's the famous open question of whether a problem whose solution can be checked quickly can also be solved quickly. With SAT, checking is easy because you just plug in a proposed answer and do the math. The hard part is finding one that works.

SAT is considered the textbook example of hard problems of this kind. A fast method for solving it would instantly make thousands of other problems fast to solve too. Most experts believe no such method exists. That belief goes by the shorthand "P does not equal NP."

The ETH goes further than that conjecture. It says not only that SAT is hard, but how hard. If the ETH falls, P could still differ from NP, so hard problems wouldn't automatically become easy.

The ETH was widely accepted as true. Hundreds of papers in graph theory, computational biology, databases, and computational geometry build on it. They show, for example, that a problem can't be solved faster than a certain time if the ETH holds.

Now OpenAI says its system has proved the ETH is false. If the proof holds, those papers lose their foundation. Their results wouldn't automatically be wrong, but they'd no longer be proven.

OpenAI says the result could help researchers find better algorithms. Turning it into practical gains would still take a lot of research, though.

The practical payoff is unclear, but the theoretical fallout would be big

SAT matters a lot in practice. Specialized programs called SAT solvers check chip designs for errors and test software, for example.

They often handle formulas with millions of variables already. That's because formulas from real-world applications are usually much easier than the worst case the ETH deals with. Speeding up only the worst case wouldn't automatically help these programs.

MIT professor Ryan Williams struck a similarly cautious tone on X. When a user asked what everyday developers would notice first, Williams said nobody knows yet. At the current pace, he said, it's plausible that practical SAT solving could see serious progress within 12 months. "Or we may see nothing of the sort. I really don't know," he admitted.

The result would also ripple through complexity theory itself, specifically the study of circuits, which are networks of simple logic gates like AND, OR, and NOT. If OpenAI's result holds, Williams says it would follow that a certain class of very demanding problems can't be solved with small circuits. "Small" here means that when the input doubles in length, the circuit needs at most about twice as many gates.

The people who came up with the ETH are checking whether it's wrong

Williams will independently check and explain the result together with Russell Impagliazzo and Ramamohan Paturi of UC San Diego. Impagliazzo and Paturi originally proposed the ETH along with Francis Zane. Williams writes that the group hasn't signed any nondisclosure agreements, is working unpaid, and plans to share interim findings as they go.

In an open letter, the three also make clear that their involvement isn't an endorsement of the claim. A result this big needs careful, independent review, they write.

At the group's request, OpenAI is publishing all the raw data, including the written proof and the Lean proof. The company has also committed to funding a conference on what the result means for the field.

A decades-old wave conjecture may now hold in every dimension

The math result concerns a conjecture about waves like those in sound, light, or earthquakes. Mathematician Christopher Sogge proposed it in 1991.

Waves can concentrate at a single spot, much like light at the focal point of a magnifying glass. The conjecture says this extreme concentration only lasts briefly. Averaged over time, waves behave more smoothly, or evenly, than the extreme case would suggest. That's why it's called the local smoothing conjecture.

Until now, it had only been proven in two dimensions, for waves on a surface like water. Guth, Wang, and Zhang did that in 2019. OpenAI says its models have now produced a proof for every dimension, including waves in space and in hypothetical spaces with even more dimensions.

OpenAI says the result reaches beyond waves. Because the local smoothing conjecture is so basic to the field, two other well-known conjectures follow from it. They are the Kakeya conjecture from geometry and Stein's restriction conjecture from Fourier analysis. Fourier analysis breaks signals like sounds into individual oscillations. Proving the local smoothing conjecture automatically proves both of these as well.

The Kakeya conjecture shows how hard even these follow-on results are. Wang and Zahl only proved it for three dimensions in 2025. According to OpenAI, both conjectures would now be solved in all dimensions.

Unlike the other two results, no dedicated group is shepherding this proof. OpenAI says it did reach out to an outside expert to discuss that kind of collaboration. On that person's advice, though, the company published the proof text and the Lean proof directly. That way, researchers can decide for themselves how to check the result.

OpenAI wants to put quantum field theory on solid mathematical ground

The physics result goes to the foundation of particle physics. Physicists describe elementary particles and the forces between them using quantum field theory, which OpenAI calls the most important framework in modern theoretical physics. Its predictions are extremely accurate, but the theories lack an exact mathematical basis.

Instead, physicists work with approximations, such as an imaginary lattice of points that they keep making finer. It's still an open question whether this produces a unique, consistent theory, meaning whether a theory "exists" in the mathematical sense. Whether it describes nature correctly is a separate question.

OpenAI says its AI has proved that certain quantum field theories exist in four dimensions, meaning three dimensions of space plus time. So far, nobody has pulled off such a proof in four dimensions for theories where particles interact with each other.

The strong force sits at the center of it. It binds quarks into protons and neutrons, which in turn holds atomic nuclei together. Particles called gluons carry it. The proof covers three theories that build on each other like steps.

The bottom step is Yang-Mills theory. It describes only gluons, without quarks. It's tied to one of the seven Millennium Prize Problems, each of which carries a $1 million prize from the Clay Mathematics Institute.

The problem has two parts. The first is proving that Yang-Mills theory exists mathematically. The second is showing that it has a so-called mass gap. OpenAI explicitly says it has solved only the existence part. That means the Millennium Problem wouldn't be fully solved.

The mass gap points to a puzzle. In the equations, gluons have no mass, and forces carried by massless particles normally reach very far. The electromagnetic force, which massless light carries, is one example. The strong force, by contrast, only acts over tiny distances, such as inside an atomic nucleus. Physicists explain this by saying gluons clump into structures that do have mass, and even the lightest of them isn't massless. The gap between zero and that smallest possible mass is called the mass gap. Computer simulations support it, but nobody has proven it mathematically.

The second step is quantum chromodynamics (QCD). It adds quarks and gives a complete description of the strong force.

OpenAI says both theories can exist mathematically mainly because of asymptotic freedom. This means the strong force gets weaker as particles get closer. That keeps the math manageable even as the lattice gets finer and finer.

The third step would normally be the Standard Model of particle physics. It describes three of the four fundamental forces, everything except gravity. According to OpenAI, though, it can't be extended to arbitrarily small distances, because some of its forces get stronger at small distances instead of weaker.

That's why the proof covers the simplest grand unified theory. It reduces the three forces to a single one and includes the Standard Model's force and matter particles. Like the strong force, this unified force can get weaker at small distances. No experiment has confirmed such theories, though.

If the proof holds, all three steps would have a mathematical foundation. That wouldn't change any of physics' predictions. OpenAI hopes it will turn quantum field theory into a mathematically rigorous discipline.

A group led by David Gross will shepherd the work. Gross shared the 2004 Nobel Prize in Physics for his work on asymptotic freedom. The group also includes Michael Douglas, Arthur Jaffe, Igor Klebanov, and Nikita Nekrasov. Jaffe helped write the Millennium Prize Problem on Yang-Mills theory.

OpenAI says it has already translated the Yang-Mills proof into Lean. Unlike the computer science group, though, this group is holding back the AI's materials for now and plans to write up the result itself.

OpenAI's review process raises questions of its own

OpenAI admits the process comes with trade-offs. Whoever picks the first shepherds helps decide who gets involved first, the company writes, and some people end up knowing more sooner than others. OpenAI also says it's not yet clear which of the three approaches works best.

OpenAI says it isn't claiming scientific credit for the discoveries. Credit should go to the groups explaining the results instead. The company appears to be responding to criticism after the PR disaster over Navier-Stokes.

OpenAI has also pledged $5 million to the Simons Foundation to fund workshops and conferences on AI results.

Williams' group also uses its open letter to call for a broader debate that goes beyond the review. The questions are how to verify AI breakthroughs, who gets access to them, and who deserves the credit.