Borsuk's conjecture
Borsuk's conjecture asserts that every bounded subset of Rd can be covered by d + 1 sets of strictly smaller diameter. A manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a counterexample in dimension nine. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- According to the manuscript's introduction, Borsuk posed the question in 1933, and Kahn and Kalai disproved it in high dimensions in 1993. Later work lowered the dimension of the smallest known counterexample. Bondarenko reached 65 and Jenrich and Brouwer reached 64, both in 2014. The introduction also cites a 2026 public proof note by Grinsztajn with a finite counterexample in dimension 63.
The original result
- Claim. Consider the rank-one orthogonal projectors onto lines in R4, with the Frobenius metric. They form a compact set of diameter √2 in the nine-dimensional affine space of trace-one symmetric 4×4 matrices. This set cannot be covered by ten subsets of strictly smaller diameter, so Borsuk's assertion fails in dimension nine. A corollary extends the construction to compact counterexamples in every dimension d ≥ 9. The manuscript states that it does not determine the smallest dimension in which the assertion fails, nor the exact number of pieces needed for its set.
- Source. A nine-dimensional counterexample to Borsuk's covering assertion in the openai/math repository (commit
1581d4c). - Formalization, as described by the repository. The scope note lean/docs/156.md states that the formalized counterexample is this projector set. It has diameter √2 and cannot be covered by ten arbitrary sets of smaller diameter. The comparator statement is BorsukNine.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 15 October 2026) |
|---|---|---|---|---|
| 2026-10-10 | acprk/openai-math-followups, note Borsuk numbers of projective-space projector sets | Use (numerical) | Partitions of the projector set by nearest line among 11 optimized lines appear valid, while 10 lines fail. Combined with the manuscript's lower bound, this suggests that exactly 11 pieces are needed for that set. The note also argues numerically that the analogous eight-dimensional set of projectors onto complex lines in C3 is not a counterexample, since 9 pieces suffice. | A GitHub note that labels its results numerical and reproducible but not yet interval-certified. |
| 2026-10-07 (merged 2026-10-11) | formal-conjectures pull request #6898 | Formal statement | Marks the repository's Borsuk statement for 4 ≤ n ≤ 62 as refuted, with a variant for n = 9, and links OpenAI's Lean proof. | Merged pull request. It notes that the link differs from the repository statement by a routine transport that is not in the linked proof. |
| 2026-10-14 | formal-conjectures pull request #7312 | Formal statement | Adds a statement that Borsuk's conjecture fails in every dimension n ≥ 9, citing the manuscript's corollary, with the proof left as a placeholder. It also proves that an isometry preserves the existence of a cover by a fixed number of sets of strictly smaller diameter. It notes that dimensions 4 to 8 remain open. | Open pull request. Its description states that Codex was used under the author's direction. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.