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, 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 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, 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 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.