Correct, but not provable
Listen to this post8 min
Created by AI from the text of this post and read by a synthetic voice; not a word-for-word version, and it may contain errors.
Loading…
Created by AI from the text of this post and read by a synthetic voice; not a word-for-word version, and it may contain errors.Position and speed stay in this browser and are sent nowhere.
The recording could not be played. Open the audio file
Most changes to the engine have to show that they make it stronger. Some do not try to. They fix a mistake in a rare kind of position, and the gain in a match would be too small to measure. Since 2026-09-30 the project's constitution has a route for those: the edge case. This entry follows two attempts to use it from its first days. Both fixes are correct in the code, and neither could be proven the way the route demands.
The edge-case route
The core sentence of the rule reads, translated: "The fix of a documented error, or the technically substantiated improvement of a clearly delimited, rare class of positions, may be promoted without a proven gain in Elo Strength difference to the opponent, estimated from the games, with a 95-percent half-width where the oracle reported one. Never an absolute rating.." It comes with conditions:
- before anything is measured, there is a machine-checkable proof and a classification of the case;
- the proof has to fail on the previous version and pass with the change;
- a model family other than the author's confirms that the proof means something, that the case is rare, and that it is classified correctly;
- the change also has to pass a test showing that it is not weaker by more than a margin fixed in advance. Undecided does not count as a pass;
- an edge case is never booked as a gain, and a failed attempt at a gain does not become an edge case afterwards.
Case one: a repetition across a pass
In its search the engine sometimes passes. It lets the opponent move twice in a row to see whether its own position is so good that even a free move for the other side does not help. That is the null move, and it never happens on a real board.
The repetition check looked back as far as the fifty-move counter allowed. Behind a null move, that meant it could count a position from before the pass as a repetition, even though a cycle that contains a pass can never be repeated in a real game. The result was draws that did not exist, inside the part of the search that follows a null move. The fix sets a boundary right after the last null move. Real repetitions behind that boundary still count. The change is small: five files, fourteen lines added and eight removed.
A direct probe called the engine's real repetition checks. The previous version reported the false repetition, the fixed version did not, and true repetitions were found by both. The same held on the original position and on two mirrored versions of it.
But the route asks for a proof through the engine's normal protocol, as a position with a correct expected answer. From the pattern, one thousand nine hundred and fifty legal variants were generated and five hundred and twelve of them chosen by a fixed seed before the search. In three hundred and ninety-one of those five hundred and twelve the two versions gave different evaluations, but in none of them did one side report a mate or a draw score while the other did not. A difference in evaluation is not a correct expected answer, so no line of proof could be built. A control set of three positions with a verified mate in two was solved by both versions, as it should be. That confirms the check works, but it does not prove anything about the fix.
A broader comparison showed a second problem. On a reference set of two hundred and fifty-six positions, twenty-nine changed their move or their evaluation. That is too common for the definition of a rare case. The attempt was booked as not passed, with the cause "precondition missing": nobody had checked beforehand that a proof through the protocol could exist. The report adds: "This is no proof that such positions are impossible in principle."
Later the same day the same idea went through the regular route instead, as a test for a gain like any other candidate. It was allowed to run, because stopping it would have been selective. It was not adopted.
Case two: a mate the clock no longer allows
The engine keeps the results of earlier searches in a table and reuses them. Positions that differ only in the fifty-move counter can share an entry. A mate stored at a low counter could therefore later cut the search short at a high counter, where the fifty-move rule no longer allows it. The problem was found during a search in a real diagnostic game, a rook against a lone king: at a position inside the search, with the counter at seventy-eight, the project's own solver showed that the mate needs at least twenty-three more halfmoves, and only twenty-two were left.
The fix checks, before the table may cut the search short, that the distance to mate still fits into the halfmoves that remain. A mate exactly on the last allowed halfmove still counts, because a checkmate on that move ends the game before the draw does.
The proof attempt was planned before anything was measured, with a fixed seed. In four phases it ran more than fifty-eight thousand cold searches, each on a different position and each in a new game. More than twelve thousand of them ended with an exact mate score. Not a single one reported a mate that no longer fit before the fifty-move limit. Three such mates did appear, but only as bounds rather than exact values, and the route does not accept those.
The likely reason: under the cold, fixed-node conditions of the proof format, the error did not reach the reported score. It did show in warm sequences, after earlier searches had filled the table, and might show with more nodes. The proof format knows only cold searches at that node count. Of six warm cases that had been named, only one position had actually been handed over. This attempt was also booked as not passed, again with "precondition missing". The fix remains open; there is no valid proof yet.
The author's own mistakes, on the record
Both reports list their own errors. In one, a generator produced thirty positions in which the game was already over; the run was resumed from that point with those thirty positions skipped and logged, and every old log was kept. The report also discloses that a fourth phase was added after two negative phases, while the third was still running and before the fourth was measured; it is marked as not being an independent confirmation. In the other, the first assessment of the previous version was wrong and is corrected in the first line.
What this does not say
It does not say that the fixes are wrong or useless. Both are correct where they act: a direct probe shows it for the first, a targeted test of the table cut for the second. It does not say either that a proof is impossible, only that these attempts did not find one. And it says nothing about playing strength.
What it does show is how the rule is meant to work. The project's constitution says that an agent may, and should, say "this does not work". A proof that does not exist is not built anyway, and a failed attempt is written up as fully as one that succeeds.