Browse › Combinatorics › 156 Borsuk's conjecture fails in dimension nine
A nine-dimensional counterexample to Borsuk's covering assertion
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
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.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-23) and not checked by a person. May be wrong or incomplete. Report an error.
Follow-up works
- acprk, Borsuk numbers of projective-space projector sets (towards dimension 8) (GitHub research notes, 2026-10-10). Reports numerical evidence for an eleven-cell nearest-line cover of the paper's projector set $X$, which with the paper's lower bound would give $b(X)=11$, and a nine-cell cover of the $\mathbb{CP}^2$ analogue, so that it is not an 8-dimensional counterexample; the note labels this "numerical, reproducible; not yet interval-certified". [AI-generated per source]
- Erdős Problem a Day, #505: Borsuk's conjecture fails in dimension nine (research report, 2026-10-20). Claims an exact rational certificate for an eleven-set cover (giving Borsuk number 11 conditional on the paper's lower bound) and a smaller set of sufficient combinatorial conditions; it also reports replaying the release's Lean proof and compiling a bridge to Formal Conjectures definitions, with referee reports attributed to Claude Opus 5.5. [AI-generated per source]
Comments and discussion
- Gil Kalai, Updates: Sharing AI progress on mathematics (amazing!); and my lecture plans (Combinatorics and more, 2026-10-07). Item 2 highlights the compact nine-dimensional counterexample and connects it to earlier discussions of the minimum counterexample dimension on the blog, while stressing that the announced results still need checking by mathematicians.
Formalization
- OpenAI math release, Lean scope notes for family 156 (lean/docs/156.md, 2026-10-06). The release's scope note: the projector set is compact, has diameter $\sqrt2$, lies in the trace-one hyperplane and admits no cover by ten arbitrary sets of smaller diameter; it links the comparator file
BorsukNine.lean. - OpenAI, BorsukNine.lean (comparator challenge) (openai/math). States
main_theoremforprojectorSet ⊆ traceOneSymmetricinEuclideanSpace ℝ (Fin 4 × Fin 4), with covers restricted to subsets of the projector set; the challenge file hassorryas a placeholder. - OpenAI, OAI/Geometry/Borsuk/Main.lean (openai/math). Contains
euclidean_nine_counterexample, a compact set inEuclideanSpace ℝ (Fin 9)of diameter $\sqrt2$ with no ten-set cover of smaller diameter, transported from the matrix statement viacoordinates9_isometry; this file itself contains nosorry. - Google DeepMind formal-conjectures, FormalConjectures/Wikipedia/BorsukConjecture.lean (formal-conjectures). Adds
borsuk_conjecture.not_nine : ¬ BorsukConjecture 9, citing this paper and linking the proof to the release'sMain.lean#L117; its docstring records dimensions 4–8 as open. - Google DeepMind formal-conjectures, FormalConjectures/ErdosProblems/505.lean (formal-conjectures). The docstring of Erdős Problem 505 (Borsuk) cites this paper as [OAI26] for failure at $n=9$ and points to
borsuk_conjecture.not_nine. - mo271 and reviewers, feat: mark problems solved in the OpenAI math release and link formal proofs (PR #6898) (google-deepmind/formal-conjectures, opened 2026-10-07, merged 2026-10-11). In review, anxkhn suggested linking the release's
EuclideanSpace ℝ (Fin 9)theorem rather than the matrix-space one; the PR notes a remainingMetric.diamvsediamand cover-definition gap between the two statements. [family-level] - bengoechea, feat(Borsuk): add the n ≥ 9 variant and isometry transport (PR #7312) (google-deepmind/formal-conjectures, opened 2026-10-14, open at time of collection). Adds the statement of the paper's Corollary 7.1 (failure for all $n\ge 9$) with
sorry, plus a proved lemma that isometries preserve small-diameter covers; the PR discloses Codex assistance.
Related prior literature mentioned by others
- Gil Kalai, Some old and new problems in combinatorial geometry I: Around Borsuk's problem (arXiv:1505.04952; Surveys in Combinatorics 2015). The Erdős Problem a Day report points to §2.4 as an earlier proposal to use the full projector configuration conditional on the double-cap conjecture, beyond §2.3 already cited by the paper.
- Henry Adams, Johnathan Bush, Florian Frick, The topology of projective codes and the distribution of zeros of odd maps (arXiv:2106.14677, 2021). The survey arXiv:2610.17090 names "Adams–Bush–Frick (2021)" as the nearest relative of the paper's odd spectral extension; the identification with this preprint is not explicit, as the survey gives no arXiv number.
- Alexander Tolmachev, Vsevolod Voronov, Reducing the upper bound for the Borsuk number in ℝ⁴ to 8 (arXiv:2605.19068, May 2026). The formal-conjectures Borsuk file cites it alongside the dimension-9 result for the still-open dimension-4 case.
- Yibo Ji, An AI Generated Counterexample to Borsuk Problem in Dimension 63 (arXiv:2608.12561, Aug 2026, withdrawn). The formal-conjectures file lists it as an independent finding of the 63-dimensional example that the paper cites as Grinsztajn2026. [AI-generated per source]
- Nick Konz, Claude Tackles Borsuk (project page, Aug 2026, updated 2026-10-19). The formal-conjectures file credits this as another independent rediscovery of the 63-dimensional example, with an exact-arithmetic certificate; the page argues the method cannot reach dimension 62. [AI-generated per source]
Possibly relevant literature (found by the agent, not checked)
- Henry Adams, Johnathan Bush, Florian Frick, Metric Thickenings, Borsuk-Ulam Theorems, and Orbitopes (arXiv:1907.06276; Mathematika 66 (2020) 79–102). Proves Borsuk–Ulam-type statements for odd maps averaged over small-diameter sets on spheres, which may relate to the paper's passage from small-diameter covers to an odd map via integration; not in the bibliography.
Digests and expositions
- Latent Seminar, Rank-one projectors and Borsuk's covering problem (expository notes, 2026-10-07). Explains the diameter identity, smooth-cover reduction, spectral extension and support-complex obstruction, expressly disclaiming a complete proof verification or Lean audit.
- Ying Xie, What the Machine Invented: Mining New Mathematical Instruments from OpenAI's October 2026 Release of AI-Generated Mathematics (arXiv:2610.17090, 2026-10-12). Section 9.3.3 summarizes family 156 as "combination leaning new", extracting the odd spectral extension, equality-case degree analysis and six-label triangle systems, and notes the example is continuous so does not settle the finite-set version in ℝ⁹; the survey states it does not verify proofs. [family-level]
News and blogs
- Wikipedia contributors, Borsuk's conjecture (Wikipedia, accessed 2026-10-21). Records OpenAI's 2026 claim of a counterexample in ℝ⁹ and notes that the construction is infinite, so it would not disprove the finite version in ℝ⁹.
- Azmat, Borsuk Conjecture: OpenAI's 9D Proof Shatters the 63-Dimension Record (BinaryVerse AI, 2026-10-12). Outlines the paper's projector construction and proof strategy and distinguishes the strict smaller-diameter condition from merely avoiding orthogonal pairs.
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 156
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:A-nine-dimensional-counterexample-to-Borsuks-covering-assertion-September-23-2026,
author = {{OpenAI}},
title = {{A nine-dimensional counterexample to Borsuk's covering assertion}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/A-nine-dimensional-counterexample-to-Borsuks-covering-assertion-September-23-2026/paper.pdf}{OAI:A-nine-dimensional-counterexample-to-Borsuks-covering-assertion-September-23-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/156.md. The Lean statements have not been checked by people against the paper's claims.
Family 156: Borsuk's conjecture fails in dimension nine
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.
This is the only paper in this family.