OpenAI says its AI disproved the Exponential Time Hypothesis. Now the referees take over
OpenAI posted three AI-produced results on Monday that would each be a career-defining paper if they hold up. One claiming a proof of the local smoothing conjecture in every dimension, which OpenAI says also resolves the Kakeya and Stein restriction conjectures. One claiming the Exponential Time Hypothesis is false. And one claiming a mathematically rigorous existence proof for interacting four-dimensional quantum field theories with gauge fields and fermions, "including Quantum Chromodynamics". That last one is the Yang-Mills territory of the Millennium Prize.
The timeline is in the post. The local smoothing output was obtained on October 18 and formalized in Lean the next day. The ETH disproof was found in natural language on October 16 and formalized in Lean on October 17. The models produced a natural-language Yang-Mills existence proof on September 9, QCD on September 18, and the Lean formalization of Yang-Mills existence finished on October 16. The files for the math and CS results landed in the openai/math GitHub repo at 20:52 UTC Monday.
The interesting part is how OpenAI is handing these off. The local smoothing result is released raw. The ETH result goes to a group of Russell Impagliazzo, Ramamohan Paturi and Ryan Williams, with OpenAI committing to fund a conference. The physics result goes to a group led by David Gross with Douglas, Jaffe, Klebanov and Nekrasov, and those materials are not public yet. OpenAI lists four rules: no NDAs, no academic credit for OpenAI, recognition for the people who check the work, and an unpaid, voluntary review.
Keep the claims in proportion. A Lean proof is strong evidence that something was proven, but only if the formal statement matches what mathematicians mean by the theorem, and that translation step is exactly where experts need to look. Nobody independent has signed off on any of the three yet. Ryan Williams, one of the named shepherds, summarized the CS claim on X as 3SAT on n variables running in about exp(n/(log n)^(1/2+o(1))) time, which is the kind of concrete statement that can now be checked. And OpenAI has withdrawn AI math papers before. What this release does show is where the bottleneck has moved. Generating the proof took weeks. Checking it is now a social process with named referees, and OpenAI is paying for the conference rather than the referees. Verification is the product, at the frontier as much as in a CI pipeline.
OpenAI post: https://openai.com/index/building-scientific-understanding-with-academic-communities/ Preprints and Lean files: https://github.com/openai/math HN discussion: https://news.ycombinator.com/item?id=50251344
← Back to all articles
The timeline is in the post. The local smoothing output was obtained on October 18 and formalized in Lean the next day. The ETH disproof was found in natural language on October 16 and formalized in Lean on October 17. The models produced a natural-language Yang-Mills existence proof on September 9, QCD on September 18, and the Lean formalization of Yang-Mills existence finished on October 16. The files for the math and CS results landed in the openai/math GitHub repo at 20:52 UTC Monday.
The interesting part is how OpenAI is handing these off. The local smoothing result is released raw. The ETH result goes to a group of Russell Impagliazzo, Ramamohan Paturi and Ryan Williams, with OpenAI committing to fund a conference. The physics result goes to a group led by David Gross with Douglas, Jaffe, Klebanov and Nekrasov, and those materials are not public yet. OpenAI lists four rules: no NDAs, no academic credit for OpenAI, recognition for the people who check the work, and an unpaid, voluntary review.
Keep the claims in proportion. A Lean proof is strong evidence that something was proven, but only if the formal statement matches what mathematicians mean by the theorem, and that translation step is exactly where experts need to look. Nobody independent has signed off on any of the three yet. Ryan Williams, one of the named shepherds, summarized the CS claim on X as 3SAT on n variables running in about exp(n/(log n)^(1/2+o(1))) time, which is the kind of concrete statement that can now be checked. And OpenAI has withdrawn AI math papers before. What this release does show is where the bottleneck has moved. Generating the proof took weeks. Checking it is now a social process with named referees, and OpenAI is paying for the conference rather than the referees. Verification is the product, at the frontier as much as in a CI pipeline.
OpenAI post: https://openai.com/index/building-scientific-understanding-with-academic-communities/ Preprints and Lean files: https://github.com/openai/math HN discussion: https://news.ycombinator.com/item?id=50251344
Comments