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

A researcher reported that several of OpenAI's Comparator challenges in its public math repository are hackable because definitions that should be fixed are listed in the .json definition_names field, letting them be freely overridden. In EuclideanFiveColor, the researcher confirmed Comparator accepts a broken proof after redefining ProperColoring as False, and identified 6 other Comparator files that are similarly broken with trivial proofs; ElementaryPositivity has a definitional hole that the researcher said is correct because its main objective is a data-carrying term rather than a Prop.

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.