OpenAI says its models proved the Exponential Time Hypothesis false, verified in Lean
OpenAI announced three new discoveries by its models and asked outside experts to check them. The biggest says the Exponential Time Hypothesis, a widely believed limit on how fast Boolean formula satisfiability can be solved is false; the proof was verified in Lean, a machine proof checker. A group led by Russell Impagliazzo, Ramamohan Paturi and Ryan Williams will verify it. A physics group led by David Gross will examine a claimed existence proof for pure Yang–Mills theory.