OpenAI says an AI proved one of computer science's biggest open problems. No independent expert has reviewed it yet.

The conjecture

Subhash Khot stated the unique games conjecture in 2002, while still a graduate student. It concerns how well computers can approximate answers to problems that have no perfect solution. In 2008, Prasad Raghavendra showed that if the conjecture is true, one classic algorithm is the best possible for a whole family of such problems.

The race

On the morning of September 11, MIT professor Dor Minzer got a text: rumors were spreading that OpenAI had found a proof and might release it any day. Minzer and his graduate students Yumou Fei and Shuo Wang had a milestone of their own — a proof, completed in April, of a "4-to-1" version of a related conjecture by Khot. Three days later they posted it, a 95-page paper, with an unusual disclaimer: "The current version of the manuscript is complete mathematically, but it is not in the shape we wished to share in."

"From section 6 onward, there are literally no connecting words," Minzer told Quanta. "We felt the need to apologize for that."

The result has a striking consequence: for a graph that can be colored with three colors, it is hard to find any valid coloring, no matter how many extra colors you allow. "You cannot do it even with the entire Crayola box," said Princeton's Mark Braverman.

"They solved the problem in the old-fashioned way, with their minds, and wrote it with their own fingers." — Ryan O'Donnell, Carnegie Mellon

What OpenAI released

On October 6, OpenAI announced a proof of the unique games conjecture "along with 376 other results across many different fields of math," including 40 other proofs in theoretical computer science. Quanta called it "the highest-profile example of an AI-generated proof in theoretical computer science to date."

The release included a machine-checked proof, verified in the Lean proof assistant, of the related 2-to-1 conjecture. Complexity theorist Scott Aaronson wrote the next day that the unique games proof also has a Lean certificate — "or at least, we're pretty sure that it's a proof!" — but that "it also appears that no human has understood just about any of these proofs yet."

Even the size of the release is hard to pin down: Quanta counted 376 other results, while Aaronson's post refers to 372 papers. As of these reports, no independent expert had reviewed the unique games proof.

What it does and doesn't prove

An announcement is not acceptance. Mathematical results are trusted after experts work through them, and that hasn't happened yet. Braverman, speaking before the release, was blunt: "Math by press release is not that healthy for math." "It's not 'one and done,'" he added.

Minzer worries about what AI removes from the process. "There is a lot of value in failing and knowing why you failed," he said. "Using AI takes all of this out." And for researchers on long projects, a new anxiety: "You don't know if you're going to get scooped by the trillion-dollar company."

What to watch

• Independent expert review of OpenAI's proof.
• The revised, fully written version of the MIT team's paper.