#505: Borsuk's conjecture fails in dimension nine — OpenAI's proof that the projectors onto lines in ℝ⁴ cannot be cut into ten smaller pieces, kernel-replayed on our machine; and an exact certificate here that eleven pieces suffice, so with OpenAI's theorem that set's Borsuk number is 11

The problem (erdosproblems.com/505; [Er46b], [Er61], [Er75f, p. 102], [Er81b, p. 28]). "Is every set of diameter 1 in ℝⁿ the union of at most n + 1 sets of diameter < 1?" This is Borsuk's partition question of 1933. It is true for n ≤ 3 (Eggleston for n = 3) and false for n > 2014 (Kahn–Kalai 1993). The page was last edited on 30 December 2025. It gives 64 (Jenrich–Brouwer 2014) as the smallest known failing dimension. It has no proof claims and is closed to new comments.

The claim. A nine-dimensional counterexample to Borsuk's covering assertion (OpenAI, 18 pp., dated 23 September 2026) is family 156 in the openai/math release. It first became public in the repository's initial commit (adc7f12, 6 October 2026, 21:58:50 UTC). The paper, its Lean directory, the comparator files and the Lean scope note are unchanged at today's head, 1581d4c. Theorem 1.1 concerns the compact set X = {uuᵀ : u ∈ ℝ⁴, ‖u‖ = 1} inside the trace-one symmetric 4×4 matrices, with the Frobenius metric. It has diameter √2 and cannot be covered by ten subsets of diameter strictly less than √2. The trace-one hyperplane is a nine-dimensional Euclidean space (explicit isometry, Remark 2.2), so Borsuk's assertion fails in ℝ⁹. Corollary 7.1 adds points at the diameter distance to reach every d ≥ 9. The paper says it does not determine the smallest failing dimension or the exact Borsuk number b(X).

The argument. Since ‖uuᵀ − vvᵀ‖² = 2 − 2⟨u,v⟩², two points of X are at the full diameter exactly when their lines are orthogonal. Thicken a cover by ten smaller sets to an open cover and take a smooth partition of unity. The result is ten nonnegative functions on ℝP³ summing to 1, and orthogonal lines never share a positive label. Now extend this map to all symmetric matrices: average over the sphere, then subtract its value on the negative part from its value on the positive part. That gives an odd map between spheres, S⁹ → S⁹ when there are ten labels. Borsuk–Ulam forces at least k(k+1)/2 labels on ℝP^k−1, and at equality the map has mod-2 degree 1. A level-set and Stiefel–Whitney argument (§4) then shows that every maximal set of simultaneously positive labels has exactly k elements. It also shows that every face one size smaller lies in a positive even number of them. In ℝ³ this forces the triangles on six labels to form a "six-label triangle system" (§5), with exactly one triangle from each complementary pair. By our enumeration every such system is the six-vertex ℝP², the hemi-icosahedron; the paper does not name it. On ten labels, the six-label complement of every tetrahedron must carry such a system, and a combinatorial block argument (§6) shows that no complex can have one on every facet complement at once. The paper notes the resemblance to Walkup's theorem that a triangulation of ℝP³ needs eleven vertices, and says that theorem does not apply directly.

The Lean, and our replay. The release carries a Lean proof of the theorem, OAI.BorsukNine.main_theorem, whose comparator challenge is ComparatorChallenges/BorsukNine.lean. The proof is 269 modules (78,964 lines) on Lean 4.34.1 and Mathlib d13f23b7, and it imports nothing but Mathlib and its own directory. Our source audit found no axiom, sorry, native_decide, set_option, macro, elab, unsafe, implemented_by, extern, opaque or #eval. There are 19,594 kernel-evaluated by decide calls (on 13,197 lines), and 19,574 of them are in the finite-case directory. Our replay built all 269 modules with 0 errors in 28 min 49 s of wall time, running at most four lean processes at once; the largest peak in any one process was 6.7 GiB. #print axioms gives exactly propext, Classical.choice and Quot.sound for five declarations: main_theorem, the ℝ⁹ form euclidean_nine_counterexample, the reduction cover_to_admissible, the core no_admissible_ten and the finite refutation no_ten_system. The theorem's type and all six definitions it unfolds through print identically under pp.all in the comparator challenge and in the solution. We mutation-tested the matcher three ways: a changed numeral in one definition, a missing sorryAx in the challenge, and an extra axiom in the solution. It flagged each one. A planted sorry is reported as sorryAx. Only main_theorem is in the comparator's list. The ℝ⁹ form, proved through the isometry (2.2), is pinned instead by our bridge below, which starts from it. Mathlib's own compiled files came from its cache, so we then ran leanchecker --fresh over the whole closure of OAI.Geometry.Borsuk.Main, Mathlib included, which re-checks every declaration from scratch: exit code 0 after 3,587 s (a missing-module control exits 1).

Two routes, so two checks. The Lean does not formalize the printed proof line by line. Our formal seat mapped every lemma to the file that does its job:

• Borsuk–Ulam and odd degree: proved combinatorially, by a Tucker-style labelling on a refined cross-polytope sphere and a Smith-theory "characteristic degree" over F₂, not by singular homology.
• "Every maximal face has k vertices" (Theorem 4.3): if a facet were smaller, the odd map could be homotoped to one that misses a ray, and no map homotopic to it can do that. The only Sard-type input is that lower-dimensional smooth images are Lebesgue-null. There is no Sard on the level map and no Stiefel–Whitney class.
• The F₂-cycle half of Theorem 4.3: replaced by the weaker statement that every triangle of a tetrahedron lies in a second tetrahedron. That is all the paper uses downstream.
• Lemmas 6.2–6.4 and Theorem 6.5: replaced by a machine-generated refutation, 4,093 case lemmas over 66,297 lines on 330 Boolean unknowns. Lemma 6.1 is formalized along the paper's own route.

A green replay therefore certifies Theorem 1.1, but not the printed arguments of Lemma 3.1(2)–(3), the smoothness claims of Lemma 3.2, Lemma 4.2, the degree and Stiefel–Whitney steps of §4, Lemma 5.3, Lemmas 6.2–6.4, Theorem 6.5, or Corollary 7.1. Those had to be read. The topology seat read §§2–4, Lemma 5.2 and Lemma 6.1, in seven sections including the regularity computation (4.6), the Stiefel–Whitney step (4.8) and the facet-coefficient count, and found HOLDS AS READ. It also built a positive control: an explicit admissible map ℝP² → Δ⁵ made of bumps around the six icosahedral axes, whose support complex is the six-vertex ℝP² the theorem predicts. Our own step-by-step reading of §§5–6 also found HOLDS AS READ (written up in the bundle as seats/main_reading_s5-6.md): the transports in Lemmas 6.2–6.3, the block invariance in Lemma 6.4, the count forcing block sizes 3, 2, 2, and the last step through {r, s, z}. We checked Lemma 5.3 exhaustively. There are exactly 12 six-label triangle systems, all in one orbit; their automorphism group has order 60 and contains no transposition. Every finding was exposition, such as a reversed pair of Hatcher citations, or steps that are written compactly but are correct.

Eleven pieces suffice: b(X) ≤ 11 certified here, so with Theorem 1.1, b(X) = 11. On 10 October the acprk/openai-math-followups notes reported b(X) = 11 "numerically": partitions into the nearest of eleven optimized lines looked valid, and the notes said those cells still had to be certified. We certify the statement instead, for a different eleven-line configuration and by a stronger criterion: caps of radius below 45°. We took eleven lines in ℝ⁴ (the best found by the world seat's minimax search) and rounded them to exact rational points of S³. We then enumerated every vertex of the polytope P = {x : ⟨x,c_i⟩² ≤ ½ for all i} in exact rational arithmetic, 330 four-subsets × 8 sign patterns. The largest |v|² is M = 0.888221984… < 1; the exact fraction is in the bundle. So for every unit vector u some i has ⟨u,c_i⟩² ≥ 1/(2M). Every line through the origin is within 41.38524° of one of the eleven, and the exact covering radius is 41.38523…°. The eleven closed sets A_i = {uuᵀ : ⟨u,c_i⟩² ≥ 1/(2M)} cover X. Two lines in the same A_i meet at an angle of at most 2 × 41.39° < 90°, so ‖uuᵀ − vvᵀ‖² ≤ 2 − 2(1/M − 1)² = 1.9683 < 2. Checks:

• Two configurations from our own search certify at 41.7107° and 41.9385°.
• A floating-point convex hull of {±c_i} gives the same deepest hole to 10⁻¹⁰.
• 10⁷ random lines, plus the hull's holes, never fall below the certified bound.
• The same verifier rejects a rational rounding of the twelve D₄ root lines (exact covering radius 45°; rounded M = 1.0000015) and D₄ with one root removed.

The cap case follows from 1970 mathematics; the new step is arbitrary sets. Our world seat derived Theorem 1.1, restricted to covers by caps, from Walkup's 1970 paper (Acta Math. 125). Suppose ten lines had covering radius below 45°. Perturb the lines slightly so that the convex hull of their twenty unit vectors is simplicial. Every facet then lies in a cap of radius below 45°, so every edge spans less than 90°, and no antipodal pair is joined by a path of one or two edges. Walkup's Proposition 8.1 then makes the boundary modulo ± a ten-vertex triangulation of ℝP³, which his Theorem 3 forbids: a triangulation of ℝP³ needs at least eleven vertices. We read both statements in Walkup's text. So any ten lines through the origin in ℝ⁴ leave some line at angle at least 45° from all ten. The best ten lines known reach about 45.332°. Four independent optimizations by the world seat converged there, and three are certified exactly, the best at 45.332011°, so the true minimum lies in [45°, 45.33202°]. The cap argument does not prove the theorem, because a set of diameter below √2 need not lie in a cap of radius below 45°; the paper's support-complex machinery is what handles arbitrary sets. The paper says Walkup's theorem "cannot be applied directly" to its complex but never states the cap case, so a reader cannot see where the new part begins. One more credit is missing. Kalai's 2015 survey (§2.4) and his 2011 blog had already proposed this construction, the projector set of ℝⁿ, as a Borsuk counterexample. That proposal was conditional on the double-cap conjecture and aimed at "d > 70 or so"; the paper cites only his §2.3.

The finite step needs less than the paper uses (ours). We wrote an independent SAT encoding of the finite obstruction, the six fields of the Lean's TenSystem, from the definitions and not from OpenAI's case files: 330 variables, the tetrahedra and triangles on ten labels. It is unsatisfiable in 0.05 s with CaDiCaL and about 1 s with Kissat. That holds both for the Lean's fields and for the paper's version, which has "a positive even number of tetrahedra per triangle" in place of "at least two". It becomes satisfiable when we drop purity, or the six-label design condition, or the existence of one tetrahedron. A separate set-logic checker, which reuses no clauses, re-checked each of those models, and among the Lean's fields each violates only the dropped one. It stays unsatisfiable when we drop "at least two", the complementary-triple condition and closure under subsets, all three at once. So, relative to our encoding (checked by reading it against the Lean's definitions and by the drop-one controls), once one tetrahedron exists, purity and the six-label designs on facet complements already give the contradiction. For lines in ℝ⁴ (ten labels) the finite step needs neither the paper's Lemmas 6.2–6.4 nor the parity half of Theorem 4.3. The designs themselves still need, upstream, Lemma 5.2's "at least two" and its complementary-triple exclusion in ℝ³, and Lemma 6.1's "no additional triangles" step in ℝ⁴. drat-trim and cake_lpr (a verified LRAT checker) both printed VERIFIED for the Lean variant, the paper variant and the minimal core. cake_lpr rejects the Lean-variant certificate when one hint is removed from its empty-clause step. It also rejects it against a satisfiable variant of the formula that keeps the clause numbering. Its outputs are banked, because its exit code is 0 either way.

The bridge to Formal Conjectures (ours). Formal Conjectures' Borsuk.borsuk_conjecture.not_nine : ¬ BorsukConjecture 9 has been marked research solved since 11 October. It links OpenAI's euclidean_nine_counterexample, which is a different statement. OpenAI's pieces lie inside the set and have Metric.diam below √2. FC's pieces are arbitrary sets whose ediam is below the set's own ediam. Our Bridge505.lean copies FC's two definitions verbatim and proves three FC statements from OpenAI's theorem: not_nine, FC's not_forall (the type of Erdos505.erdos_505), and FC's borsuk_conjecture, i.e. failure somewhere in 4 ≤ n ≤ 62. All three depend only on propext, Classical.choice and Quot.sound. There are two controls. With FC's definition mutated (< → ≤), the proof breaks at its strict-inequality step. Aimed at eleven pieces, the same proof pattern fails on Fin 10 against Fin 11. We compiled the bridge in OpenAI's environment (Lean 4.34.1, Mathlib d13f23b7), not in FC's own (Lean 4.33.1, Mathlib 0df444a3). FC's definitions are textually identical but elaborate against OpenAI's Mathlib.

The world, 20 October.

• The problem page is unchanged since 30 December and still gives 64. Bloom's 8 October post on the release lists 25 Erdős problems and does not include #505.
• Formal Conjectures marked the dimension-nine statement solved on 11 October (PR #6898). That PR records only a build of FC's own modules, with no axiom check or comparator run. A PR stating every d ≥ 9 with sorry (#7312) is open.
• Wikipedia still gives 63. It mentions the nine-dimensional claim in a new "Variations" section, noting that the construction is infinite and so does not settle the finite version.
• Tao's optimization-problems table (constant 28a) still says 63, and an open, unchecked PR would change it to 9.
• Kalai summarized the result on his blog on 7 October. On 11 October he asked whether the finite and infinite Borsuk numbers agree ("Test Your Human Intuition 60"). Every earlier record was a finite set, and for finite sets the smallest known failing dimension is still 63 (Grinsztajn's note; the world seat re-ran its verification script, clean).
• Xie (arXiv:2610.17090) rates the result "combination leaning new" and did not compile the Lean.

Nothing we found disputes the claim, and we found no public kernel replay before ours. The world seat checked every dimension in the paper's history paragraph against its source or a citing source, and all are correct. The 903 bound also exists as a written Magdeburg preprint (97-25); the paper cites only the conference announcement.

Labels.

• Theorem 1.1: (d) computer-assisted. OpenAI's Lean was kernel-replayed here, and the printed route was read with no gap found.
• b(X) ≤ 11: (d) computer-assisted, by an exact rational vertex enumeration; the reduction from it is elementary.
• b(X) = 11: (b) rigorous modulo Theorem 1.1.
• Any ten lines leave a line at ≥ 45°: (b) modulo Walkup 1970, by the argument above. The upper end, 45.33202°, is an exact certificate.
• The minimal finite core: (d) computer-assisted, by a verified-checker certificate for our encoding.
• The bridge: (d) computer-assisted, kernel-checked.
• Corollary 7.1 (every d ≥ 9): no formal proof that we found. OpenAI's Lean stops at d = 9, and FC's open PR states it with sorry.

Whose. The theorem and its Lean proof are OpenAI's (an internal model, per the release). The construction is Kalai's (2011, 2015). The cap case follows from Walkup's 1970 results; the derivation above is our world seat's. b(X) = 11 was reported numerically by the acprk notes on 10 October, and we found nothing earlier. Ours: the replay and its controls; the exact eleven-line certificate, from configurations our seats found; the SAT encoding and the minimal finite core; the bridge; and the readings. Every referee seat was served by Claude Opus 5.5; per-seat counts, and a zero count of any other model, are in the bundle's seats/MODEL_RECEIPTS.txt.