OpenAI's latest internal reasoning model has unveiled ten remarkable mathematical advances.
Including:
- First proved the existence of non-sofic groups;
- Provided new circuit lower bounds;
- Overcame the difficulty limit of the Closest Vector Problem (CVP);
- And the quantum parallel repetition theorem for two-player quantum games with exponential decay.
What matters most to Columbia University associate professor Henry Yuen is the last one—
In 2016, Yuen made significant progress on this issue but did not fully resolve it. Over the past decade, he faced repeated failures, and even a month ago, he used ChatGPT 5.5 to make another attempt at the ultimate proof, with minimal results.
And AI, on his shoulder, gave the ball a light kick, sending it into the goal.
The proof was correct, but humans didn't understand.
A few days ago, Lijie Chen sent a draft of a paper to Henry Yuen and several other people.
Back then, life was too busy for him to delve deeply into it. Now that the paper has been published, he can’t hold back—he has something to say.
The quantum parallel repetition theorem, a field Henry Yuen spent years researching during graduate school, is his most proud achievement.
Henry Yuen is currently an Associate Professor of Computer Science at Columbia University, Srivani Family Chair.
He remembered those afternoons spent in cafés, late nights at the office, and countless weekends that should have been restful, repeatedly deconstructing and studying Ran Raz’s classic parallel repetition theorem.
He was unable to sleep, tossing and turning, determined to solve the quantum version of this theorem. He consumed vast quantities of mathematical tools and ultimately succeeded in proving polynomial decay.
https://arxiv.org/pdf/1604.04340
More importantly, he built confidence from it, finally recognizing his own capabilities and proving that he could indeed solve some of the problems (at least a portion) that others also cared about.
He believes OpenAI's proof is likely correct, given that it has already been formally verified in Lean. However, Henry Yuen still needs some time to fully absorb this new proof.
Although the new proof builds upon where his previous one left off, the AI surpassed the limitations of his original proof strategy by employing certain techniques and methods that may already be known to researchers in operator theory and functional analysis.
Beyond excitement, Yuen's first reaction was disappointment—with the writing style of the paper.
He said the proof sounded entirely AI-generated: overly long and meandering in its setup, with key points appearing like magic tricks, leaving the reader confused.
The proof from OpenAI is interesting to read, yet somewhat perplexing.
It first places the problem squarely on the table, then suddenly leaps to the idea of "using a precondition to find the correct purification," leaving almost no logical steps in between.
Next comes a series of rather unconventional matrix entropy calculations, winding through complex computations until finally concluding that this path is viable.
But it doesn't explain where that most crucial step—the intuition—comes from.
And the most ingenious, most creativity-demanding stroke—the technique of using the Uhlmann transformation to expand the operator space—should have been the most stirring climax of the entire proof, yet the AI discarded it like sand and gravel, abandoning it in Section 4 without warning or explanation.
The correct proof hides the most important idea.
He hopes OpenAI can use a few more prompts to thoroughly organize this draft.
More painful is the second layer: Lean verification passing does not equal understanding.
The machine can guarantee that every step of reasoning is flawless, but it cannot answer questions like: “Why does this approach work?”, “What does it mean in the broader theoretical landscape?”, or “Where else can it be applied?”—Lean can’t address any of these.
Yuen admitted that he is still processing this proof.
The answer was right in front of him, yet he had to painstakingly reconstruct the AI’s unspoken intuition, line by line, as if reading a layperson’s paper.
Yes, there is a Lean proof there, but it’s just formalization—it doesn’t mean I understand it. True comprehension will likely take time to sink in.
Indeed, AI has expanded the boundaries of human understanding—but then what? What remains of the joy and meaning of research? If AI solves all the problems he has been deeply obsessed with, what is left for him?
Questions kept coming. But one thing became increasingly clear to him: the mathematician’s days ahead would be anything but idle—he’d need to tame these intellectual giants and translate their jargon into plain language.
AI "falsifies" century-old mathematical conjecture exposed as fake! Lean is not a safe box.
Last week, Ramana Kumar refuted the most famous unsolved problem in mathematics, the Collatz conjecture, using 300 lines of Lean.
It asks a very simple question: Given a positive integer, repeatedly apply these two rules—divide by 2 if it’s even, multiply by 3 and add 1 if it’s odd—will you always eventually reach 1, no matter which number you start from?
You can calculate:
This conjecture states that no matter which positive integer you start with, you will eventually fall into the 4→2→1 cycle.
Since mathematician Lothar Collatz proposed this problem in 1937, no one has been able to prove it true or find a counterexample.
It was called by mathematician Paul Erdős: “Mathematics is not yet ready for such problems,” and American Academy of Sciences member and mathematician Jeffrey Lagarias believes it is “an extraordinarily difficult problem, far beyond the reach of contemporary mathematics.”
If falsified, it would undoubtedly be a groundbreaking news in the mathematical community.
Unfortunately, three days later, this formal Lean proof was invalidated, as it actually exploited a low-level vulnerability in Lean’s kernel.
Daniel Selsam from OpenAI, along with an AI specialized in cybersecurity, assisted Lean FRO in conducting a kernel audit.
As a result, they discovered more than one vulnerability within the Lean kernel!
Around the same time, Alex Kontorovich, a mathematics professor at Rutgers University and advisor to the Lean Specialized Research Organization, posted a warning: Don’t treat Lean as an all-purpose verifier.
He struck right at the core—semantic alignment.
Even if the Lean kernel is flawless, Lean only handles code compilation. Who ensures that the "definitions" you write in code align with the "intuitive intentions" expressed in natural language?
Lean can confirm only one thing: that the code compiles and the formal logic is sound. But it does not verify a far more critical question: Does this formal statement actually correspond to the theorem you intended to prove?
The proof is correct, but the problem was copied incorrectly—Lean still gives a green light.
However, this alignment issue cannot be resolved solely by computers.
In his 2026 ICM talk, Kontorovich pointed out that the biggest blind spot in formalized mathematics is not getting the derivation right, but getting the wording right. Ultimately, human experts must be the ones to verify it.
The Liquid Tensor Experiment achieved its legendary status precisely because researchers conducted an almost obsessive manual review of every mathematical definition.
When viewed together, the two professors’ statements point to the same truth: AI can demonstrate, machines can verify, but understanding and oversight remain human responsibilities.
Finally, here’s a bit of gossip about AI inference models:
Reference materials:
https://www.henryyuen.net/posts/on-openai-and-quantum-parallel-repetition/
https://x.com/AlexKontorovich/status/2083919186825236831
https://x.com/henryquantum/status/2083623700608237956
This article is from the WeChat public account "New Intelligence Yuan," author: ASI Revelation; editor: David