OpenAI Says Its AI Model Refuted the Exponential Time Hypothesis

OpenAI says an internal AI model has refuted the Exponential Time Hypothesis, a conjecture about how hard it is to solve Boolean satisfiability that hundreds of computer science results rely on, the company announced. OpenAI said the model found the disproof on Oct. 16 and that it was checked in the Lean proof language the next day. It published the write-up and Lean proof on GitHub.

Russell Impagliazzo and Ramamohan Paturi of UC San Diego, two of the researchers who proposed the hypothesis, will lead an independent examination with Ryan Williams of MIT. "Our involvement should not be taken as certification of the claim," they wrote, The Next Web reported. Williams said the group signed no nondisclosure agreements and is not being paid.

OpenAI announced two more results. It says its models proved the local smoothing conjecture in every dimension, which would also settle the Kakeya and restriction conjectures, and produced a proof that certain quantum field theories, including pure Yang-Mills theory, exist in four dimensions. A physics group led by Nobel laureate David Gross will review that work and decide when to release it. OpenAI said it does not seek academic credit for the results.