Report: Six Hidden AI Test Levels Have No Solution, Chinese Team Says

Researchers at Tsinghua and Zhejiang universities say they have mathematically proved that all six sealed levels of the AI benchmark ARC-AGI-3 are unwinnable, according to a report by the Chinese tech outlet Pandaily. ^[1]

The claim is unconfirmed and rests on a single report. If it holds, it would mean that the machines which failed those levels were not failing at all, or at least not in the way the scoreboard implies.

What the researchers say they did

According to Pandaily, the team built what it calls an algebraic world model. A world model is a system's internal picture of how an environment behaves: press this, and that follows. Here, the model reportedly learned the rules of ARC-AGI-3's games from the games themselves. ^[1]

The team then wrote those rules down in Lean 4 and used them to prove that all six sealed levels cannot be completed, the report says. ^[1] Pandaily also reports that frontier models, the most capable systems the big labs have built, failed to solve the same six levels. ^[1]

What the benchmark is for

ARC-AGI-3 tests whether a system can be dropped into an unfamiliar interactive game, work out the rules by exploring, and find a way to finish. No instructions come with it. The point is to measure the kind of fresh reasoning that memorized training data cannot supply.

Sealed levels are the guard against cheating. They are not publicly available for practice, so a model cannot have seen them in advance. They are meant to show how a system performs on tasks nobody could have prepared for.

A level with no solution would be a strange thing to find in that set. A test of ingenuity is only fair if ingenuity can succeed.

What Lean 4 can and cannot vouch for

Lean 4 is a proof assistant, a program that checks a logical argument one step at a time and accepts it only if every step follows from the definitions and assumptions given. It does not get tired, and it does not take anyone's word for anything. A proof that Lean accepts is correct relative to what was typed in.

That qualifier carries the weight here. Lean cannot tell whether the rules the researchers typed in match the rules the benchmark actually runs. If the learned model of a game differs from the real game in some small way, a flawless proof would still be a proof about the wrong game.

Lean also cannot say whether the assumptions are fair, or whether "unwinnable" means what a benchmark designer would mean by it.

That last point is the first thing a reader should ask. The word could mean no sequence of moves ever completes the level under the game's rules. It could mean none does within a stated action or resource limit. Those are very different claims, and the report as described does not say which one the researchers are making.

What is not yet known

The researchers' names have not been established, and no paper, code or proof file has been pointed to that outsiders could examine. The date of the Pandaily report is also unclear.

Which frontier models were tested, under what conditions, and what "failed to solve" meant in the evaluation are all open. So is how the team checked that its formalized rules match each sealed level.

The benchmark's organizers have not been heard from in anything the paper has seen.

The result is also separate from earlier coverage. The Daily Inference has reported on Memento 3's claimed success on ARC-AGI-3's 25 public games. That concerned the games anyone can practice on. This claim concerns the six that are kept hidden, and one does not verify the other.

Why it matters if it holds

The report points to a distinction that benchmark builders will recognize. Learning how a game works is not the same as being able to win it. Failed attempts, however many, can never show that a level has no solution, because the next try might always be the one that works. A formal proof, if its rules are the right ones, can show that no sequence of moves wins.

There is a wider lesson in that, and it is my view, not the researchers'. Benchmarks are increasingly used to rank the most expensive machines in the world. If a hidden level can be shown to have no answer, it was never measuring the machine. Every score attached to it would need rereading.

If the claim fails, it is still instructive. A proof built on a subtly wrong model of the rules would show how easily a polished formal result can be about the wrong thing. Either way, the next step is simple and public: the proofs and the rule definitions need to be put where others can run them.