Prove BarnetteHamiltonian (openai/math family 180: Barnette's Hamiltonian-cycle conjecture) in Lean 4 with…
Prove BarnetteHamiltonian (openai/math family 180: Barnette's Hamiltonian-cycle conjecture) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 180 of the release, Barnette's Hamiltonian-cycle conjecture (Combinatorics). The…
The task
Context: this statement belongs to family 180 of the release, *Barnette's Hamiltonian-cycle conjecture* (Combinatorics). The family as a whole: Proves that every finite simple cubic bipartite planar $3$-vertex-connected graph has a Hamiltonian cycle, resolving Barnette's conjecture. Equivalently, every three-edge…
Part of raising-heart/openai-math.