Smallest dimension in which Borsuk’s conjecture fails

Upper bound, last-listed row

| $63$ | [[Gri2026](#Gri2026)] | Current best: a $321$-point subset of $\mathbb{R}^{63}$ whose smaller-diameter subsets have size at most $5$, so at least $65>64$ parts are required. |tracked since 2026-07-24 — no movement seen yet

Lower bound, last-listed row

| $4$ | [[Per1947](#Per1947)], [[Egg1955](#Egg1955)], [[Gru1957](#Gru1957)] | Borsuk’s conjecture is true for $n\le 3$. After the $63$-dimensional construction, the first possible failing dimension remains open for $4\le n \le 62$. [WX2022-lb-nle3] |

exact pinned row

| $4$ | [[Per1947](#Per1947)], [[Egg1955](#Egg1955)], [[Gru1957](#Gru1957)] | Borsuk’s conjecture is true for $n\le 3$. After the $63$-dimensional construction, the first possible failing dimension remains open for $4\le n \le 62$. <a href="#WX2022-lb-nle3">[WX2022-lb-nle3]</a> |

tracked since 2026-07-24 — no movement seen yet

Checked against material for its cited source

• Another row, not one shown above: bound row $65$ line 62 citing [Bon2014] — the claim we checked: that the cited 2014 paper gives the upper bound this row lists, 65, through a two-distance set of 416 points on the 64-dimensional sphere in 65-dimensional space that cannot be partitioned into 83 sets of smaller diameter, as the row's comment says. The row's second link, [Bon2014-ub-65], is checked only for whether it points at that statement. What we read supports it: Theorem 1 gives a two-distance set of 416 points on the unit sphere in 65-dimensional space that cannot be partitioned into 83 parts of smaller diameter, so b(65) ≥ 84 and Borsuk's conjecture fails in dimension 65; the row's second link quotes that theorem. source link (read in the journal edition, Discrete & Computational Geometry 51 (2014), pp. 509–515, as the publisher's full-text page, which carries no page numbers, and checked against the arXiv preprint version 3: the abstract and Theorem 1). Selected: drawn by its position in the list of cited rows, not because it looked wrong.

1 bound row(s) here have been checked against material for their cited source (1 drawn by position, 0 chosen because something already looked wrong). Across this whole ledger 70 row(s) have been drawn by position, against 691 rows that name a source, counted on 2026-09-27: 64 were checked against material for their cited sources and for 6 the cited source could not be read at all. 5 more were chosen for suspicion and checked; they are counted apart, because a set selected for suspicion carries no rate. A row not listed here has NOT been checked.

Outside the source table: a claim in OpenAI's math release

• Family 156, “Borsuk's conjecture fails in dimension nine”, claims that Borsuk's conjecture fails in dimension 9.

  Its Lean statement, BorsukNine.lean:

  theorem main_theorem : IsCompact projectorSet ∧ projectorSet ⊆ traceOneSymmetric ∧ Metric.diam projectorSet = Real.sqrt 2 ∧ ¬ HasTenSmallCover

  The file's set is the 4 × 4 matrices u·uᵀ for unit vectors u in four dimensions. The statement places it among the symmetric matrices of trace 1, a flat 9-dimensional slice with the usual distance, gives its diameter as √2, and says it cannot be split into 10 pieces of smaller diameter. Since 10 = 9 + 1, that is a counterexample in dimension 9, against 63 in this constant's last-listed upper-bound row. Reading the slice as 9-dimensional is our step; the statement file does not state it.

  Status: a Lean statement of it is published with a proof by its authors. We read the statement and it matches this constant's definition; we have not compiled the proof, and we have not read the paper.

A claim in a preprint release, read at openai/math@fd4aeeb on 2026-10-12. It is not in the source table, and this ledger has not changed the rows above because of it.