Borsuk's conjecture

The question

borsuk_conjecture. Borsuk's conjecture, open range: every bounded subset of ${\mathbb{R}}^n$ with at least two points can be partitioned into $n+1$ sets of strictly smaller diameter, for $4\le n\le 62$.

The conjecture is known to be true for $n\le 3$ and false for $n\ge 63$.

borsuk_conjecture.four. Borsuk's conjecture in dimension $4$, the smallest open case.

In 1933 Karol Borsuk [Bo33] asked whether every bounded subset of ${\mathbb{R}}^n$ can be partitioned into $n+1$ sets, each of strictly smaller diameter. The hypothesis that the answer is positive became known as Borsuk's conjecture.

The conjecture is true for $n=2$ [Bo33] and $n=3$ [Pe47, Eg55]. It is false in general: Kahn and Kalai [KK93] disproved it for $n=1325$ and for all $n>2014$. Bondarenko [Bo14] gave a counterexample in dimension $65$, and Jenrich and Brouwer [JB14] one in dimension $64$, the smallest refereed counterexample. In 2026 Grinsztajn [Gr26] posted a 321-point counterexample in dimension $63$, obtained with AI assistance and verified by exact computation; the same configuration was found independently by Konz and by Ji [Ji26]. The cases $4\le n\le 62$ are open. In dimension $4$, every bounded set can be partitioned into $9$ parts of smaller diameter [La82], and a 2026 preprint reduces this to $8$ parts [TV26].

Erdős Problem 505 (FormalConjectures.ErdosProblems.«505») points to this file.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.BorsukConjecture (2 statements).

theorem borsuk_conjecture (n : ℕ) (hn : 4 ≤ n) (hn' : n ≤ 62) : BorsukConjecture n

theorem borsuk_conjecture.four : BorsukConjecture 4

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• Wikipedia
• [Bo33] Borsuk, K. (1933). Drei Sätze über die n-dimensionale euklidische Sphäre. Fundamenta Mathematicae 20, 177–190. https://doi.org/10.4064/fm-20-1-177-190
• [Pe47] Perkal, J. (1947). Sur la subdivision des ensembles en parties de diamètre inférieur. Colloquium Mathematicum 2, 45.
• [Eg55] Eggleston, H. G. (1955). *Covering a three-dimensional set with sets of smaller diameter*. Journal of the London Mathematical Society 30, 11–24. https://doi.org/10.1112/jlms/s1-30.1.11
• [La82] Lassak, M. (1982). An estimate concerning Borsuk partition problem. Bulletin of the Polish Academy of Sciences, Mathematics 30(9–10), 449–451.
• [KK93] Kahn, J., Kalai, G. (1993). A counterexample to Borsuk's conjecture. Bulletin of the American Mathematical Society 29(1), 60–62. https://arxiv.org/abs/math/9307229
• [Bo14] Bondarenko, A. (2014). On Borsuk's conjecture for two-distance sets. Discrete & Computational Geometry 51(3), 509–515. https://doi.org/10.1007/s00454-014-9579-4
• [JB14] Jenrich, T., Brouwer, A. E. (2014). *A 64-dimensional counterexample to Borsuk's conjecture*. Electronic Journal of Combinatorics 21(4), P4.29. https://doi.org/10.37236/4069
• [Gr26] Grinsztajn, M. (2026). A 63-dimensional counterexample to Borsuk's conjecture. Proof note and verification script, https://github.com/maaxgrin/borsuk-63-counterexample
• [Ji26] Ji, Y. (2026). An AI generated counterexample to Borsuk problem in dimension 63. https://arxiv.org/abs/2608.12561 (withdrawn as a duplicate of [Gr26])
• [TV26] Tolmachev, A., Voronov, V. (2026). *Reducing the upper bound for the Borsuk number in ${\mathbb{R}}^4$ to 8*. https://arxiv.org/abs/2605.19068
• [OP28a] Tao, T. et al., Optimization problems, constant 28a (smallest Borsuk counterexample dimension). https://teorth.github.io/optimizationproblems/constants/28a.html
• [Ka15] Kalai, G. (2015). *Some old and new problems in combinatorial geometry I: Around Borsuk's problem*. https://arxiv.org/abs/1505.04952

Source and licence

Imported from Formal Conjectures (Wikipedia), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.