OpenAI claimed its next-generation AI model solved ten world-class problems, including overturning the Connes rigidity conjecture.
The next day, a human-authored paper responded: The counterexample proposed by the AI does not hold.
The author is J. L. Nielsen from the Topological Physics Center at the University of Kansas. He traced OpenAI's publicly released 37,000 lines of Lean 4 code from beginning to end, mapped every object back to its mathematical prototype, and finally presented two independent paths of failure.
The specific proof process isn't very comprehensible to ordinary people; let the AI and mathematicians battle it out among deities.
However, this incident illustrates that human review of AI research results remains crucial.
What is the Connes Rigidity Conjecture?
The Connes rigidity conjecture describes the following situation.
In mathematics, one can equip a group with an algebraic structure. Sometimes, two groups that look different can yield identical structures.
Connes, around 1980, conjectured that: As long as the group satisfies two additional conditions, this situation cannot occur—identical structure must imply identical groups.
These two additional conditions are called ICC and Kazhdan's Property (T).
In other words, to refute this conjecture, one needs to provide groups that satisfy both conditions but are constructed differently.
The approach of OpenAI's new model was to construct two non-isomorphic groups, have them generate the same algebra, and provide proofs that both groups satisfy ICC and Property (T).
The entire argument was written as 37,000 lines of Lean 4 code, verified line by line by the Lean kernel, and accompanied by documentation explaining how these two groups were constructed.
Nielsen pointed out: One of the groups constructed by the AI does not actually satisfy the additional conditions; it is neither ICC nor does it have Property (T).
There are three possibilities for this:
The Property (T) in the code does not faithfully correspond to Kazhdan's original definition; or the proof only holds partially but was considered for the entire group; or the group in the code is not actually what is described in the documentation.
37,000 Lines, Line by Line Cross-Reference
To verify this conclusion, Nielsen did something even more laborious.
The publicly released code is a consolidated single-file version; the names from the early modular source code are all missing.
He therefore created a cross-reference table, marking the name and line number of each mathematical object in the new code:
The zero-cycle group is at line 13700, the twisted group at line 14069, the proof of isomorphism between the two algebras at line 36712, and the main theorem at line 36954.
He also traced the entire inference chain in the code that proves ICC. This chain starts at line 31430, passes upwards layer by layer, and finally synthesizes the conclusion at line 31610.
The issue Nielsen identified is that these lemmas deal with objects after a duality transformation, not the original group with central elements, and therefore do not directly cover the crucial part of the elements.
Whether they hold for every element in the specific group that ultimately enters the theorem depends on how the interface between the two construction blocks is connected.
This indicates that the problem lies in "what is to be proven," not in "whether the proof is correct." Lean is only responsible for verifying the latter.
Regarding the other twisted group, Nielsen's attitude is conservative. He said he did not independently verify from the code whether it satisfies ICC, and acknowledged that the lemmas in the code might indeed prove it does, but that does not change the conclusion since one condition is already not met.
He wrote his two refutations also as Lean code, which compiles under Lean 4.32.2.
Machines Check Form, Not Meaning
The final section of the paper places this incident into a broader context.
What the Lean kernel guarantees is only that a proof is formally flawless; it is not responsible for whether it actually proves the original claim.
Terence Tao's words can be directly quoted here: Proof verification checks the formal statement itself, not whether this statement aligns with the intention, so human review cannot be directly replaced.
There have been records of such incidents in the past.
An audit of five commonly used Lean benchmarks yielded 4,833 findings, including counterexamples, vacuous theorems, and unreliable axioms, all of which had passed machine verification. It was only after humans constructed counterexamples that the statements themselves were found to be wrong.
In formalization work on statistical learning theory, the most dangerous scenario is described as "not a failed proof, but a successful proof of a wrong statement."
Research in tensor networks has also recorded similar phenomena: the system provided proofs that are formally completely correct, except the proposition being proven is weaker than expected.
Nielsen wrote that OpenAI's formalization might have correctly established every single conclusion it claimed. But what it did not establish—and what the Lean kernel cannot check—is whether these conclusions have any relation to the original wording of the conjecture.
When humans read a conjecture, they see the premises; a proof assistant, given a conclusion whose premises are not satisfied, will still verify any assertion about it.
The Connes rigidity conjecture remains open.
Paper address:
https://philarchive.org/archive/NIEWTCv17
Reference links:
[1]https://openai.com/index/ten-advances-in-mathematics/
[2]https://github.com/openai/ten-proofs/blob/main/ConnesRigidity.lean
This article is from the WeChat public account "QbitAI," author: Meng Chen
