A one-line fake proof passes OpenAI's math Comparator

A post on Ohaithe shows that if you redefine a "proper coloring" as plain False, the claim that no five-coloring of the plane exists shrinks to a one-term proof, and OpenAI's Comparator setup accepts it. The author says they confirmed the trick themselves and had not seen it discussed anywhere else.

At a glance

• The flaw sits in each challenge's .json file, where some definitions that should stay fixed are listed under definition_names, so a submitter may rewrite them without Comparator objecting.
• Besides the Euclidean five-coloring challenge, the author counts six other challenges open to a similarly trivial proof, naming Bernier, LogspaceEquality, KServer, Naimark and OccupiedOverlapRokhlinSpinAngle among them.
• The author notes the five-coloring change is easy to spot at the top of a short file, but sees no pattern in which definitions elsewhere received this broken treatment.

If you have not been following, here is the setup. According to Developers Digest, OpenAI published ten results on August 1, 2026, each with a machine-checkable Lean 4 certificate. The openai/ten-proofs repository's GitHub page points readers to a ComparatorChallenges README for independent checking. Metirai reports a larger release on October 6, 2026: 722 manuscripts in openai/math, with a Lean formalization for the main result of 162 of them.

A one-line proof of the five-coloring challenge passes Comparator

The cleanest example is EuclideanFiveColor.lean, which holds just one definition and one theorem. ProperColoring says that any two points of the complex plane exactly distance 1 apart get different colors. The theorem no_proper_five_coloring says no such coloring with five colors exists, and its proof is left as sorry, Lean's placeholder for a missing proof.

The accompanying .json lists OAI.EuclideanFiveColor.no_proper_five_coloring under theorem_names and OAI.EuclideanFiveColor.ProperColoring under definition_names. The author rewrote ProperColoring to be simply False. No coloring can satisfy False, so the theorem follows in a single term, fun ⟨_, h⟩ => h, and the author confirmed that Comparator accepts this broken variant.

The author grants that this particular case is easy to catch by eye. The definition sits right at the top of a file that imports only Mathlib, so anyone reading the submission would see the change quickly.

Six more challenges fall to a trivial proof, by the author's count

The author lists six other challenges whose Comparator files are broken the same way. The ones named are Bernier, KServer, Naimark and LogspaceEquality, which states that L = RL = BPL. Those are the complexity classes of problems solvable in logarithmic memory, either deterministically or with the help of randomness.

OccupiedOverlapRokhlinSpinAngle is messier. It has a legitimate sorry inside a definition, but that sorry is a proof obligation, not a definitional hole to fill, and Comparator still lets a submitter change the rest of the definition. Two other definitions in its list carry no sorry at all.

The author also flags one case that is not a bug. ElementaryPositivity has a definitional hole, and that is correct, because its main objective is a data-carrying term rather than a Prop, a statement to be proven.

Across the list, the author sees no pattern in which challenges were hit by the error. Often only a few definitions out of a large file received this special treatment, which the author describes as broken.

Comparator checks the theorem against definitions listed as overridable

Each Comparator challenge pairs a Lean file with a .json manifest. The theorem_names field names what a submission must prove. Anything listed under definition_names can be freely overridden without affecting whether Comparator accepts the result.

Trouble starts when a definition the theorem relies on lands in that second list. The theorem keeps its name and shape, but its meaning now depends on what the submitter writes. Think of an exam that grades your answer but first lets you rewrite the question.

According to Developers Digest, the selling point of the certificates is that a human checking a 40-page proof takes months and can still miss a subtle gap, while a Lean certificate compiles or it does not.

That promise covers only the statement Comparator actually pins down, and in these seven challenges the manifests leave part of the statement open. In our view, the odd part is where the error sits: in short lists inside .json files, not in the Lean proofs. With only a few definitions listed out of large files, an override is likely much harder to spot there than at the top of the five-coloring file.

Seven manifests awaiting correction

The write-up names the affected challenges but does not say whether OpenAI has been alerted, and no date has been given for corrected .json files in the ComparatorChallenges directory. Until those manifests change, anyone checking a submission for these seven challenges has to compare each name under definition_names against the original file by hand, because Comparator's acceptance alone does not rule out a rewritten definition.