Prove BorsukNine (openai/math family 156: Borsuk's conjecture fails in dimension nine) in Lean 4 with…
Prove BorsukNine (openai/math family 156: Borsuk's conjecture fails in dimension nine) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 156 of the release, Borsuk's conjecture fails in dimension nine (Combinatorics). The…
The task
Context: this statement belongs to family 156 of the release, *Borsuk's conjecture fails in dimension nine* (Combinatorics). The family as a whole: Constructs a compact subset of $\mathbb R^9$ that cannot be covered by ten sets of strictly smaller diameter, disproving Borsuk's covering assertion already in dimension…
Part of raising-heart/openai-math.