OpenAI's 372-result math dump includes an AI proof of the Unique Games Conjecture

What happened

On October 6, OpenAI published 372 mathematical results produced by an AI model, and the list includes a proof of the Unique Games Conjecture (UGC), one of the most consequential open problems in theoretical computer science. The batch was assembled on the recommendation of an advisory group of distinguished mathematicians including Timothy Gowers and Edward Witten, according to Scott Aaronson, who covered the release in a post titled "The Mathocalypse" on his blog Shtetl-Optimized. In his assessment, it ranks among the biggest single days in the history of mathematics.

There is a catch. Aaronson writes that a Lean proof certificate exists for the UGC result, as it does for some but not all of the 372 papers, yet essentially none of these proofs have been understood by any human so far. A race to read, verify and explain the work has only just begun.

What the UGC proof contains

The UGC, posed by Subhash Khot, implies that a large family of optimization problems remains NP-hard even when you only want an approximation slightly better than what semidefinite programming relaxation, a standard tool, already delivers. Aaronson's wife, complexity theorist Dana Moshkovitz, has worked toward proving it for essentially her entire career; Aaronson recounts their nine-year-old announcing that a robot had "cooked" her.

Moshkovitz's first read of the proof, relayed by Aaronson, is blunt. The paper is written so unclearly that it cannot be read without AI assistance, and she used an AI assistant to assemble completeness and soundness claims for a central noise gadget by combining statements scattered across the document. The proof introduces a strange new recursive code with a noise test, in her description neither the long code nor the short code but something "alien". She also notes that the release contains direct optimal NP-hardness-of-approximation proofs for the conjecture's flagship applications, Max Cut and all constraint satisfaction problems, that bypass the UGC entirely.

Aaronson points to two consolations for researchers in her position: the conjecture turns out to be true, which many colleagues doubted, and everyone working on crisply stated problems is now in the same boat.

The rest of the haul

Any one of the other results could have anchored a normal year in its field, Aaronson argues. The highlights he lists include L = BPL, collapsing probabilistic and deterministic logspace; integer multiplication and the Fourier transform in less than O(n log n) time, around O(n log^0.9999999999999 n), breaking a barrier that had stood since the 1960s; a positive solution to the Unitary Synthesis Problem that Aaronson posed with Greg Kuperberg in 2007, the opposite of what most researchers expected; a proof that parity is not in QAC0, open since 1999; a near fourth-power separation between randomized and quantum query complexity for total Boolean functions; an area law for 2D gapped Hamiltonians; matrix multiplication in O(n^2.25), notable for reaching a rational exponent via a new route; a Ω(n^3) lower bound on the determinantal complexity of the permanent; a randomized polynomial-time algorithm for approximately counting perfect matchings; and a proof that solving polynomial equations over the rationals is uncomputable, arguably the biggest open problem in computability theory. There is also reported partial progress toward the Riemann hypothesis, the Hodge Conjecture and the Birch–Swinnerton-Dyer Conjecture.

What is missing is telling: no P versus NP, no P = BPP, and no separation of NEXP from P/poly, which Aaronson says is not for lack of trying.

Two ways to publish a machine proof

The evening before OpenAI's release, Virginia Williams and Josh Alman posted an arXiv preprint solving 3SUM in O(n^1.9992) time and all-pairs shortest paths in O(n^2.9995) time, refuting conjectures about those problems that had held for roughly half a century. According to Aaronson, the crucial idea came from an Anthropic model, but Anthropic handled the release differently, giving the two researchers the opportunity to write and announce a digested version in exchange for compensation.

Aaronson sketches the trade-off between the two emerging models. The OpenAI approach, dumping raw proofs publicly, sets off a competitive and largely thankless human scramble to digest and explain them. The Anthropic approach puts a private company in the position of choosing which mathematicians become the emissaries of AI discoveries. He adds that the system behind the 372 results was reportedly not a bespoke swarm of thousands of agents burning millions of dollars of compute.

Why it matters

If the Lean certificates hold up, mathematics has crossed a threshold where machines can produce formally verified results that no human yet comprehends. The bottleneck moves from proving to reading, and the human contribution shifts toward problem selection, vision and interpretation, the future Moshkovitz herself sketched. How AI proofs enter the literature, and who earns credit for digesting them, are now live institutional questions, with two very different corporate models already competing to set the norm.