OpenAI dropped 700 machine-written math papers at once. Mathematicians are not okay

On October 6, OpenAI posted a GitHub repository full of mathematics written by an unreleased internal model. The model had been handed roughly 4,000 open problems. What came back was 722 manuscripts, revised a day later to 719 grouped into 372 results, after OpenAI withdrew three papers over a sign error and patched 14 more.

The headline claim is a proof of the Unique Games Conjecture. Subhash Khot posed it in 2002, and a big chunk of theoretical computer science has been built on top of it, as an assumption, ever since. Other entries claim progress on Mahler's conjectures in convex geometry and on problems in operator algebras.

"Someone who's on psychedelics"

Scott Aaronson called it the "Mathocalypse" on his blog. His wife, the complexity theorist Dana Moshkovitz, has spent her career on the Unique Games problem. Her verdict on the proof, sent by text: it reads like it was written by someone who's on psychedelics. She ended up asking an AI to collect claims scattered across the paper so she could follow the argument.

Correctness may turn out to be the easier question. The Unique Games proof comes with a Lean certificate, meaning a proof assistant has checked a formal version of it, and about 42% of the top-line results have Lean formalizations of their main claims. A Lean check still leaves a human job: someone has to confirm the formal statement says what the paper says it does. Aaronson's own read was that no human appeared to have understood just about any of the proofs yet.

That's the odd new spot mathematics is in. The bottleneck used to be finding proofs. Now it may be reading them. Some mathematicians have called for a boycott of OpenAI, according to The Decoder, and their anger is mostly about the dump itself: hundreds of hard-to-read papers released in one go, with the field left to sort them out.

Sources: Scott Aaronson, The Decoder, Implicator.