---

OpenAI, A nine-dimensional counterexample to Borsuk's covering assertion, OpenAI Math Release preprint, 23 September 2026, linked above at the pinned revision. Let $X$ be the set of matrices $uu^{\mathsf T}$ for unit vectors $u\in\mathbb R^4$, the orthogonal projectors onto the lines of $\mathbb R^4$, with the Frobenius metric. The paper's Theorem 1.1 proves that $X$ is a compact subset of the trace-one affine hyperplane of the symmetric $4\times4$ matrices, a nine-dimensional Euclidean space; that its diameter is $\sqrt2$, attained exactly by projectors onto orthogonal lines; and that no ten subsets of $X$ of diameter strictly less than $\sqrt2$ cover $X$. Scaled by $1/\sqrt2$, $X$ is a set of diameter $1$ in $\mathbb R^9$ that is not the union of at most $n+1=10$ sets of diameter $<1$. So the answer to the question is no, and the statement already fails at $n=9$.

The argument is topological, not the Frankl--Wilson route of Kahn and Kalai. A cover by ten sets of smaller diameter is enlarged to an open cover, and a partition of unity turns it into a map from $\mathbb{RP}^3$ to the nine-simplex under which orthogonal lines have disjoint sets of positive coordinates. The map is extended by integration to positive semidefinite matrices and made odd on all symmetric matrices; the mod-two degree of the resulting odd map between spheres, with local preimage counts, forces every maximal support to have exactly four labels and the tetrahedral faces to form a cycle. A finite combinatorial argument on the six-label systems that each tetrahedron induces on its complement then yields the contradiction. Corollary 7.1 adjoins $d-9$ further points, pairwise and from $X$ at distance $\sqrt2$, to obtain a compact counterexample in every dimension $d\ge9$; that corollary has no Lean counterpart. The paper determines neither the least dimension in which the assertion fails nor the exact number of parts that $X$ needs. The corpus records the theorem at Theorem 1.1 and the corollary at Corollary 7.1 of the source card.

Formal verification. The release's Lean development, the lean/ folder at the pinned revision linked above, states the theorem as OAI.BorsukNine.main_theorem in OAI/Geometry/Borsuk/Counterexample.lean: projectorSet is compact, lies in traceOneSymmetric, has Metric.diam equal to Real.sqrt 2, and HasTenSmallCover fails. From it, OAI.BorsukNine.euclidean_nine_counterexample in OAI/Geometry/Borsuk/Main.lean derives a compact X : Set (EuclideanSpace ℝ (Fin 9)) with Metric.diam X = Real.sqrt 2 and no Fin 10-indexed family of subsets of X that covers X with every Metric.diam below Real.sqrt 2. The second declaration is the one that states the nine-dimensional claim in Mathlib's own terms; the first sits in the sixteen-dimensional matrix space and reaches dimension nine only through the trace-one hyperplane, whose isometry with $\mathbb R^9$ is proved in Main.lean rather than stated in the theorem. Empty pieces are allowed, so a cover by fewer than ten pieces counts as a cover by ten, and every piece lies in the compact $X$, so Mathlib's convention that an unbounded set has diameter zero cannot arise. The corpus's verification built both declarations and checked their axioms: each uses only propext, Classical.choice and Quot.sound. The comparator challenge lean/ComparatorChallenges/BorsukNine.lean pins the statement of main_theorem, and the pinned fingerprint was identical at the build. The only step outside Lean is the scaling by $1/\sqrt2$, a similarity.

Acceptance. The evidence is formalized: the kernel-checked proof whose statement the corpus audited and built as described above. The release attributes its manuscripts to an unreleased internal OpenAI model and names no individual author, so the claimant is the organization; its README says that the manuscripts were produced by an internal OpenAI model and are at different stages of verification. No referee and no outside reviewer has examined the manuscript as recorded here, and the site's label credits Kahn and Kalai and Jenrich and Brouwer, whose results had already answered the question no. This claim lowers the smallest known failing dimension from 64 (published) and 63 (unpublished claims) to 9.