Constructs a compact subset of ℝ9 that cannot be covered by ten sets of strictly smaller diameter, disproving Borsuk's covering assertion already in dimension nine. The example consists of rank-one orthogonal projectors onto lines in ℝ4, with the Frobenius metric. (Lean)
Manuscript
A nine-dimensional counterexample to Borsuk's covering assertion
September 23, 2026 · source · Lean formalization available · cite as \cite{OAI:A-nine-dimensional-counterexample-to-Borsuks-covering-assertion-September-23-2026}
The compact set of rank-one orthogonal projectors on ℝ4, with the Frobenius metric, cannot be covered by ten sets of strictly smaller diameter. It therefore gives a counterexample to Borsuk's conjecture in dimension nine.
Result 156 · Combinatorics. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.
Source: https://github.com/openai/math/blob/main/CONTENTS.md