The smallest dimension of a counterexample to Borsuk's conjecture: failure in dimension nine
Borsuk (1933) asked whether every bounded set of positive diameter in can be covered by subsets of strictly smaller diameter. Kahn and Kalai disproved this in high dimensions in 1993, and the smallest known failing dimension then fell through 946, 561, 323, 321, 298, 65 (Bondarenko) and 64 (Jenrich-Brouwer, 2014) to 63 (Grinsztajn, 2026). What is the smallest dimension in which Borsuk's assertion fails, and can the record of 63 be lowered substantially?
- Result
- Disproved(see note)
- Status
- Partial result
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- Discrete geometry; Borsuk partition problem
- Posed by
- K. Borsuk, Drei Satze uber die n-dimensionale euklidische Sphare, Fundamenta Mathematicae 20 (1933)
- Year posed
- 1933
- Years open
- 93y
- Solved
- 2026-09-23
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 30 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: the compact set of rank-one orthogonal projectors , a unit vector, with the Frobenius metric, lies in the nine-dimensional affine space of trace-one symmetric matrices, has diameter and cannot be covered by ten sets of smaller diameter, so Borsuk's assertion fails in dimension 9 (the record was 63). A corollary extends this to compact counterexamples in every dimension . Not shown: the smallest failing dimension (dimensions 4 to 8 remain open) or the exact Borsuk number of the set. The witness is a continuum, not a finite point set.
What the AI did
Produced by an unreleased internal OpenAI model as part of an OpenAI evaluation on open research problems, published in the openai/math release (pinned commit adc7f12). The release README says the vast majority of results used one fixed procedure, averaging about three hours of ChatGPT Pro thinking compute per result; this result is not among the README's stated exceptions (the Riemann zeta zero-free region work and the Hodge conjecture for CM abelian varieties). The manuscript is authored as OpenAI with no human author named. The main theorem has a Lean formalization in the release (Comparator challenge BorsukNine).
Verification
No independent mathematician has checked this yet. Checked here: abstract, introduction and Theorem 1.1 of the TeX source, read against Borsuk's question. Lean-checked on the release's Comparator challenge BorsukNine (declaration OAI.BorsukNine.main_theorem, listed in lean/formalization.yaml). Its statement was read here: the image of the unit sphere of R^4 under , inside the Euclidean space of 4x4 matrices, is compact, lies in the trace-one symmetric matrices, has diameter , and admits no cover by ten subsets each of diameter less than . That is the headline; that trace-one symmetric matrices form a nine-dimensional affine space is elementary and not itself stated. Not rebuilt here. The paper says it does not determine the smallest failing dimension.