# I’d like to alert people that several of the comparator challenges are noticeably broken and…

> Source: <https://blog.ohaithe.re/post/829974396980641792>
> Published: 2026-10-09 05:54:25+00:00

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:

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.