OpenAI Submits Three AI Proofs for Expert Review

OpenAI claims that its models have achieved three ambitious results: the existence of certain quantum field theories in four dimensions, a proof that would invalidate the ETH in computer science, and the resolution of a local smoothing conjecture in all dimensions with corollaries. The company has published the data, recoded proofs in Lean, and commissioned researchers to arbitrate their validity. However, several stakeholders warn that these claims require independent verification and that some aspects, such as the mass gap in Yang-Mills, are not addressed.

Physics: 4D existence claimed, mass gap remains open

OpenAI asserts that its AI has established the mathematical existence of certain quantum field theories in four dimensions, a type of proof that no previous work had achieved for theories with interacting particles. The result is positioned on the foundations of particle physics, a field where quantum field theory, described by the company as a major framework, offers very precise predictions without a fully rigorous mathematical basis. Physicists resort to approximations, such as refined point lattices, and the question remains whether these procedures lead to a unique and mathematically coherent theory, regardless of its fidelity to nature.

The announced construction unfolds in stages. First is the Yang-Mills theory, which describes only gluons without quarks and is one of the seven Millennium Prize Problems, each with a million-dollar reward. The problem links the proof of existence of the theory and the proof of a mass gap; OpenAI specifies that it only addresses the existence part, meaning the Millennium Problem would not be fully resolved. The paradox of the range of the strong force is noted: although gluons are massless in the equations—like light for electromagnetism that acts over long distances—the strong force only operates at very short ranges, which the community explains by the formation of effective structures that have mass, defining a mass gap that has yet to be mathematically proven but is supported by simulations.

The second stage is quantum chromodynamics, which adds quarks and aims for a complete description of the strong force. According to OpenAI, the mathematical existence of Yang-Mills and QCD would primarily stem from asymptotic freedom, with the weakening of the interaction at short distances keeping calculations manageable even when the lattice is refined. The third stage would normally be the Standard Model, which covers three of the four fundamental forces excluding gravity, but OpenAI indicates that it cannot be extended to arbitrary dimensions.

Review Procedure: no NDA, data released, experts commissioned

Ryan Williams, along with Russell Impagliazzo and Ramamohan Paturi (UC San Diego), is conducting an independent review and explanatory work. He clarifies that the trio has not signed any non-disclosure agreement, is not being compensated, and will publish interim results, while emphasizing that their involvement does not equate to validation and that such a dossier requires careful examination. At the request of this group, OpenAI has made the raw data available online, including proof writings and their Lean versions, and has committed to funding a conference dedicated to the implications.

The company states that it adapts its setup according to disciplines and has recoded proofs in Lean, a language that allows for step-by-step computer verification. This verification does not exclude error, as it only pertains to the statement as formalized; experts are still needed to confirm that the formalization accurately captures the intended problem. For the local smoothing conjecture, no oversight group is in place: OpenAI explains that it consulted an external expert and, on their advice, directly published the text and Lean proof for the community to choose its verification modalities. OpenAI also indicates that it is mobilizing external specialists for all verifications.

Complexity: ETH claimed false and implications for circuits

The computer science aspect targets the Exponential Time Hypothesis (ETH), which posits that the worst-case scenario for SAT remains exponential with the addition of variables. This position sharpens the boundary between P and NP by quantifying the difficulty of SAT. Even if ETH were to fall, P could still remain different from NP, and problems deemed difficult would not automatically become easy. The hypothesis was widely accepted and serves as a pillar for hundreds of papers establishing conditional bounds.

OpenAI claims that its system has proven the falsehood of ETH. If this proof holds, works based on ETH would lose their foundation without being ipso facto refuted. According to Ryan Williams, maintaining this result would have implications in circuit theory: a certain class of demanding problems would not admit small circuits, in the sense that, by doubling the input size, the number of gates could not remain bounded by about a doubling. In the background, SAT is at the heart of P versus NP: verifying a proposition is quick, but finding an assignment that satisfies the formula is difficult; each variable doubles the search space, and for 100 variables, the number of cases reaches a size of 31 digits.

SAT in practice: large-scale solvers and caution on quick gains

SAT occupies a central place in engineering, with solvers that control integrated circuits and participate in software testing, often on instances with millions of variables. These industrial cases are generally much more manageable than the worst theoretical cases, so an improvement targeting only the worst case would not automatically translate into benefits on the ground.

Ryan Williams calls for caution: he believes it is too early to say what developers would concretely see and considers only the hypothesis of substantial progress in practical SAT resolution within the next 12 months to be plausible. He adds that it is equally possible that nothing of the sort will be observed and states that he does not know.

Harmonic Analysis: local smoothing in all dimensions and corollaries

The mathematical result targets the local smoothing conjecture, formulated in 1991 by Christopher Sogge for waves such as sound, light, or seismic shocks. It postulates that while extreme concentration can occur at a point, the time average of the phenomenon is more uniform. Until now, the proof existed only in two dimensions, thanks to a result obtained in 2019 by Guth, Wang, and Zhang.

OpenAI claims to have produced a valid proof in all dimensions, including for waves in space and in higher-dimensional spaces. The company also asserts that two major conjectures would follow from this: the Kakeya conjecture in geometry and the Stein restriction conjecture in Fourier analysis, the latter studying the decomposition of a signal into oscillations. The difficulty of Kakeya is illustrated by a 2025 result from Wang and Zahl, limited to three dimensions; according to OpenAI, these two conjectures would be resolved in all dimensions if local smoothing were established.