OpenAI asks outside experts, including a Nobel laureate, to check proofs its AI produced in math, computer science, and physics

OpenAI has asked outside experts to check proofs its internal AI models produced in math, computer science and physics, saying the manuscripts are raw research data that still needs to be understood.

• The computer science result claims the Exponential Time Hypothesis is false, a hypothesis hundreds of papers in graph theory, computational biology, databases and computational geometry build on.
• OpenAI says it translated the math and computer science proofs into Lean, a language that lets a computer check every step, though Lean only checks the statement as written, not whether it captures the intended problem.
• Ryan Williams of MIT will check the result with Russell Impagliazzo and Ramamohan Paturi of UC San Diego, who proposed the ETH with Francis Zane; Williams writes that the group signed no nondisclosure agreements, is working unpaid and plans to share interim findings.
• The three say in an open letter that their involvement is not an endorsement, and at their request OpenAI is publishing all the raw data, including the written proof and the Lean proof.
• OpenAI also committed to funding a conference on what the result means for the field, and says the result could help researchers find better algorithms, though practical gains would still take a lot of research.