HF RL Explorer

Prove IndependentSets (openai/math family 106: Hardness of coloring three-colorable graphs) in Lean 4 with…

Prove IndependentSets (openai/math family 106: Hardness of coloring three-colorable graphs) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 106 of the release, Hardness of coloring three-colorable graphs (Theoretical…

The task

Context: this statement belongs to family 106 of the release, *Hardness of coloring three-colorable graphs* (Theoretical computer science). The family as a whole: It is NP-hard to color a three-colorable graph using any fixed number $c\ge3$ of colors. More strongly, for every fixed $0<\delta<1/3$, a deterministic…

Part of raising-heart/openai-math.