The Daily Model

You hand a machine a problem that has stood for thirty years. It returns a proof. The proof is formatted, structured, and formalized in a language designed to catch errors. And then you face a question no one in the field has had to answer before: what do you do with a result that no human produced?

On October 26, 2026, OpenAI announced three discoveries its models claim to have made: a proof of the local smoothing conjecture in all dimensions, a refutation of the Exponential Time Hypothesis, and a rigorous existence proof for quantum chromodynamics in four dimensions (OpenAI, October 26, 2026).

The ETH result is the one that stops you. The Exponential Time Hypothesis has been assumed true for decades. Hundreds of papers derive conditional hardness results from it—across graph theory, computational biology, databases, computational geometry. OpenAI says its system found a natural language disproof on October 16, 2026, formalized it in Lean the next day, and then reached out to the people who originally proposed the hypothesis: Russell Impagliazzo and Ramamohan Paturi at UC San Diego, along with Ryan Williams at MIT, who will lead verification (OpenAI, October 26, 2026).

There is something almost literary about asking the authors of a conjecture to referee its refutation. OpenAI frames its manuscripts as "raw research data" and admits it does not yet know which release strategy will work best (OpenAI, October 26, 2026). For the ETH result, the natural language proof and Lean formalization are public on GitHub. For the physics result, David Gross's group has chosen to withhold the AI artifacts entirely and write things up themselves.

The company states it seeks no academic credit, that participation is voluntary and unpaid, and that collaborators' conclusions are their own (OpenAI, October 26, 2026). It has committed to funding a conference on the ETH result's implications and contributed $5 million to the Simons Foundation for workshops helping researchers navigate AI-produced results.

None of this constitutes independent verification. The Lean formalizations are published, but no external confirmation of their correctness appears in the announcement. The shepherding groups have been formed; whether they have begun substantive review is not stated. OpenAI itself acknowledges that choosing initial shepherds "necessarily shapes who gets involved first and creates asymmetry of information."

The question is not whether the machine can be convincing. The question is whether a field can metabolize a proof it did not generate—whether verification scales when the author has no office hours, no reputation to stake, no career that suffers if the Lean file contains a subtle gap. Impagliazzo, Paturi, and Williams now carry that weight, and their reputations are very much in the room. The rest of us wait, read the GitHub repository, and see whether the answer holds.