Prove SnakyConditional (openai/math family 187: Snaky in 21 Maker moves) in Lean 4 with Mathlib; graded by…
Prove SnakyConditional (openai/math family 187: Snaky in 21 Maker moves) in Lean 4 with Mathlib; graded by…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 187 of the release, Snaky in 21 Maker moves (Combinatorics). The family as a whole…
The task
Context: this statement belongs to family 187 of the release, *Snaky in 21 Maker moves* (Combinatorics). The family as a whole: Settles the Snaky achievement problem: Maker can force the six-cell Snaky shape within 21 of its own moves on the initially empty infinite square board. Maker moves first, each player claims…
Part of raising-heart/openai-math.