# Several of the comparator challenges in OpenAI release are broken and hackable

> Source: <https://blog.ohaithe.re/post/829974396980641792/id-like-to-alert-people-that-several-of-the>
> Published: 2026-10-09 07:16:13+00:00

08 10 / 2026

I’d like to alert people that **several of the comparator challenges are noticeably broken and hackable**. Afaik this hasn’t been talked about elsewhere yet. The issue is that many definitions that should be treated as fixed are given in the definition_names field of the .json, meaning they can be freely overridden. For instance, in [EuclideanFiveColor.lean](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/EuclideanFiveColor.lean), the entire content is just

def ProperColoring (colorCount : ℕ) (coloring : ℂ → Fin colorCount) : Prop := ∀ point otherPoint : ℂ, ‖point - otherPoint‖ = 1 → coloring point ≠ coloring otherPoint theorem no_proper_five_coloring : ¬ ∃ coloring : ℂ → Fin 5, ProperColoring 5 coloring := by sorry

At the same time, the [.json](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/EuclideanFiveColor.json) lists:

“theorem_names”: [ “OAI.EuclideanFiveColor.no_proper_five_coloring” ], “definition_names”: [ “OAI.EuclideanFiveColor.ProperColoring” ],

meaning that the definition of ProperColoring can be freely changed without affecting Comparator’s acceptance. I confirmed that I can get Comparator to accept a broken variant of this proof, where all I need to prove is:

def ProperColoring (colorCount : ℕ) (coloring : ℂ → Fin colorCount) : Prop := False theorem no_proper_five_coloring : ¬ ∃ coloring : ℂ → Fin 5, ProperColoring 5 coloring := fun ⟨_, h⟩ => h

Now in this case, it’s pretty straightforward to check that the definition [is the right one](https://github.com/openai/math/blob/main/lean/OAI/Geometry/PlaneColoring/Coloring.lean), because it’s right at the top of a file that imports only Mathlib. But there are 6 other cases where the Comparator file is similarly broken with a trivial proof:

- Bernier [.lean](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/Brenier.lean) ,[.json](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/Brenier.json)
- LogspaceEquality (that L=RL=BPL) [.lean](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/LogspaceEquality.lean) ,[.json](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/LogspaceEquality.json)
- KServer [.lean](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/KServer.lean) ,[.json](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/KServer.json)
- Naimark [.lean](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/Naimark.lean) ,[.json](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/Naimark.json)
- OccupiedOverlap
- Rokhlin
- SpinAngle - this one has a legitimate sorry in a def, but it’s a proof obligation, not a definitional hole to fill, and Comparator lets you freely change the rest of the definition; and besides there are two other definitions with no sorry still in the list.

Worth noting that [ElementaryPositivity](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/ElementaryPositivity.json) has a definitional hole but that’s correct, they have a data-carrying term as their main objective instead of a Prop (fine).

I don’t see any pattern in what was subject to this error, and often only a few definitions out of a large file are given this special, broken, treatment.

## Also reported by

- blog.ohaithe.re: I’d like to alert people that several of the comparator challenges are noticeably broken and… <https://blog.ohaithe.re/post/829974396980641792>