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

A researcher reported that several comparator challenges in OpenAI's math repository are broken and hackable because definitions that should be fixed are listed in the definition_names field of the .json files, allowing them to be freely overridden. The researcher confirmed Comparator accepts a broken variant of EuclideanFiveColor.lean in which ProperColoring is redefined as False, and identified six other similarly broken cases: Bernier, LogspaceEquality, KServer, Naimark, OccupiedOverlap, Rokhlin, and SpinAngle. The issue matters because the challenges can be passed with trivial proofs rather than the intended mathematics.

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.