Mathematicians refuted the conjecture that OpenAI claimed to have solved within 24 hours! "The AI got every single sentence correct, but the result is completely irrelevant to the original conjecture."

OpenAI claims that its next-generation AI model has solved 10 world-class problems, including disproving the Connes Rigidity Conjecture.

The very next day, a human paper responded: The counterexample proposed by AI is invalid.

The author is J. L. Nielsen from the Center for Topological Physics at the University of Kansas. He traced all 37,000 lines of Lean 4 code publicly released by OpenAI from start to finish, mapped every object back to its mathematical prototype, and finally found two independent failure paths.

The specific proof process is too obscure for ordinary people to understand, so we can just let the AI and mathematicians conduct their own academic debate.

But this incident shows that human review of AI-generated scientific research results remains critical.

What Is the Connes Rigidity Conjecture

The Connes Rigidity Conjecture describes the following scenario.

Mathematically, an algebraic structure can be assigned to a group. Sometimes two groups that appear completely different can produce exactly the same assigned structure.

Connes put forward a conjecture around 1980: If a group satisfies two additional conditions, this situation will never happen. If the structures are identical, the groups must be identical.

The two additional conditions are called ICC and Kazhdan's Property (T) respectively.

In other words, to disprove this conjecture, one needs to construct two groups that meet both conditions but have different structures.

The approach of OpenAI's new model is to construct two non-isomorphic groups that generate the same algebra, and provide a proof that both groups satisfy ICC and Property (T).

The entire argument is written in 37,000 lines of Lean 4 code, verified line by line by the Lean kernel, and accompanied by a documentation explaining how the two groups are constructed.

Nielsen pointed out: One of the groups constructed by AI does not actually meet the additional conditions, it is neither ICC nor has Property (T).

There are three possible reasons for this:

The Property (T) defined in the code does not faithfully correspond to Kazhdan's original definition; or the proof only holds for part of the group but is incorrectly extended to the entire group; or the group in the code is not what is described in the documentation at all.

37,000 Lines, Line by Line Verification

To verify this conclusion, Nielsen completed an even more laborious task.

The publicly released code is a single integrated file version, and all the naming information from the early modular source code is missing.

So he created a comparison table, marking the name and line number of each mathematical object in the new code one by one:

The zero upper cocycle group is at line 13700, the twisted group is at line 14069, the proof of isomorphism of the two algebras is at line 36712, and the main theorem is at line 36954.

He also traced the entire reasoning chain of the code proving ICC. This chain starts at line 31430, passes up layer by layer, and finally draws the conclusion at line 31610.

The problem Nielsen pointed out is that these lemmas deal with objects after dual transformation, not the original group with central elements, so they do not directly cover the key part of elements.

Whether they hold for every element in the specific group that finally enters the theorem depends on how the interface between the two constructions is connected.

This means there is a problem with "what is to be proven", rather than a problem with "whether the proof is correct". Lean is only responsible for verifying the latter.

For the other twisted group, Nielsen took a conservative attitude. He said he did not independently verify from the code whether it satisfies ICC, and also admitted that the lemmas in the code may indeed prove that it satisfies ICC, but that does not change the conclusion — since one condition is already unmet, the counterexample to the conjecture is invalid.

He also wrote his two refutations into Lean code, which compiles successfully under Lean 4.32.2.

Machine Checks Form, Not Meaning

The last section of the paper puts this incident in a broader context.

What the Lean kernel can guarantee is only that a proof is formally rigorous, not that it can actually prove the original intended conclusion.

We can directly quote Terence Tao's statement: The proof verifies the formal statement itself, not whether this statement matches the intended meaning, so human review cannot be directly replaced.

Such accidents have been recorded in the past.

An audit of five commonly used Lean benchmarks found 4,833 issues, including counterexamples, vacuous theorems and unreliable axioms, all of which passed machine verification. It was not until humans constructed counterexamples that the proven statement itself was found to be wrong.

In the formalization work of statistical learning theory, the most dangerous scenario is described as "not a failed proof, but a successful proof of a wrong statement".

Research on tensor networks has also recorded similar phenomena: the proof given by the system is completely correct in form, but the proposition it proves is weaker than the expected target proposition.

Nielsen wrote that OpenAI's formalization may have correctly established every conclusion it claims. But what it has not established, and what the Lean kernel cannot check, is whether these conclusions are related to the original statement of the conjecture.

When a human reads the conjecture, they can identify the prerequisites, but when a proof assistant gets a conclusion that does not meet the prerequisites, it will still verify any assertion about that conclusion as valid.

The Connes Rigidity Conjecture remains an open problem.

Paper link:

https://philarchive.org/archive/NIEWTCv17

References:

[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 Official Account QbitAI, written by Meng Chen, and published with authorization from 36Kr.