---

Andriy Bondarenko, On Borsuk's conjecture for two-distance sets, Discrete Comput. Geom. 51 (2014), no. 3, 509--515, published online 5 March 2014; the preprint arXiv:1305.2584 was first posted on 12 May 2013, this page's date. The paper answers Larman's question whether Borsuk's assertion holds for two-distance sets. Its Theorem 1 states that there is a two-distance subset $\{x_1,\dots,x_{416}\}$ of the unit sphere $S^{64}\subset\mathbb R^{65}$, with $\langle x_i,x_j\rangle=1/5$ or $-1/15$ for $i\ne j$, that cannot be partitioned into 83 parts of smaller diameter. The set is the Euclidean representation of the strongly regular $G_2(4)$ graph with parameters $(416,100,36,20)$ on the eigenspace of dimension 65. The diameter is attained exactly by non-adjacent vertices, so a part of smaller diameter is a clique, and the chain of subconstituents (Hall--Janko graph, $U_3(3)$ graph, co-Heawood graph, which has no triangles) shows that the cliques have at most five vertices. So at least $\lceil 416/5\rceil=84$ parts are needed where the question allows $n+1=66$, and scaled to diameter $1$ the set answers the question no in dimension 65. The paper's Corollary 1 extends the bound to the Borsuk numbers of two-distance sets in higher dimensions, and its Theorem 2 gives a second two-distance set, of 31671 points on $S^{781}$, from the $Fi_{23}$ graph.

Depends on. No page of this wiki.

Acceptance. The result is refereed: Discrete and Computational Geometry published it. The site's label, DISPROVED (LEAN), credits Kahn and Kalai with the disproof and Jenrich and Brouwer for the smallest dimension it records, and names no source for dimension 65, so no curator credit is recorded here. The question was already answered no by Kahn and Kalai; this result settles it again in dimension 65, and the dimension-64 set of Jenrich and Brouwer is built from 352 of its vectors.

Formalization. The formal-conjectures file BorsukConjecture.lean, to which the problem's statement file points, states the failure in dimension 65 as borsuk_conjecture.not_sixty_five, credits it to this paper, and attaches as its formal proof the Lean development linked above, in a fork of that repository. The fork's proof files name the construction as Bondarenko's 416 vectors of the $G_2(4)$ graph in $\mathbb R^{65}$, with native_decide used for the large finite graph facts. This corpus has not built it, so it gives no formalized evidence here.