Borsuk’s conjecture fails in dimension 9 (OpenAI claim, Lean-checked)

Your AI and this story

Key facts

• Claim (abstract, verbatim): ‘The compact set of rank-one orthogonal projectors on ℝ⁴, 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.’
• Scope (paper, §1): ‘The theorem does not determine the smallest dimension in which it fails or the exact value of b(X).’ Corollary 7.1 adds points at distance √2 to get compact counterexamples in every dimension d ≥ 9. ‘Covers and partitions give the same number’, so the result is the partition form of Borsuk’s question
• Geometry: ‖Pₓ − P_y‖² = 2 − 2⟨u, v⟩², so ‘two projectors are at this distance exactly when their lines are orthogonal’. A cover by ten smaller sets would give ten nonnegative functions on ℝP³, summing to one, with orthogonal lines never sharing a positive label. An odd map on symmetric matrices, mod-two degree, ‘triangle systems on six labels’ and a combinatorial block argument on ten labels then give the contradiction
• Record before: 63 (Max Grinsztajn with GPT-5.5 Pro, May 2026, 321 points), 64 (Jenrich–Brouwer, 2014), 65 (Bondarenko, 2014). The construction is classical: Kalai’s 2015 survey (§2.3) lists ‘the image of all unit vectors’ under x ↦ x ⊗ x, and says (§2.4) that the double-cap conjecture, if true, would make this set a Borsuk counterexample ‘for d > 70 or so’. Kalai on 21 Oct: ‘The construction itself is one of the constructions Jeff and I studied’. ‘What is new is the proof that this set cannot be covered by ten sets of smaller diameter’
• Gil Kalai (blog, 21 Oct): ‘One of the 700 or so papers released by Open AI on October 6, 2026 asserts that f(9)>10. This is a major progress on the Borsuk’s problem. (Of course, the proof needs to be carefully checked. The main theorem has also been formalized in Lean.)’ And: ‘The topology here looks more complicated and the proof looks very beautiful!’
• Finite sets: Gábor Damásdi, commenting on Kalai’s post (21 Oct), reports that ChatGPT showed him ‘that every finite subset of its non-10-colorable example is actually 8-colorable!’ He partitions S³ by the coordinate hyperplanes into 16 regions, giving opposite regions the same colour (Kalai: ‘a very nice argument’). Kalai’s ‘Test Your Human Intuition 60’ (11 Oct) asks whether the finite and infinite Borsuk numbers agree; on 21 Oct he conjectured that g(d) < f(d) ‘for every large d’. Wikipedia’s article (checked 29 Oct) still gives 63 and says the infinite construction would not disprove the finite version in ℝ⁹
• Lean: comparator challenge BorsukNine.lean states main_theorem: the projector set is compact, lies in the trace-one symmetric matrices, has Metric.diam = √2, and has no cover by ten subsets of diameter < √2. OpenAI’s Main.lean also proves an ℝ⁹ form (euclidean_nine_counterexample). Accepted in oai-math-revised’s Comparator run of 25–26 Oct (414 of 416 challenges accepted, none rejected); accepted means the proof matches the challenge statement with standard axioms, not that a person has checked that the statement says what the paper claims
• Independent replay: Erdős Problem a Day, a tracker built by Patrick White with Claude, reports (#505, 20 Oct) that it built OpenAI’s 269 Lean modules (78,964 lines) with 0 errors and that leanchecker --fresh exited 0. Its referee seats, all served by Claude Opus 5.5, read the printed argument and found it ‘HOLDS AS READ’. It also gives an exact certificate that eleven pieces suffice, so b(X) = 11 if Theorem 1.1 holds (the acprk/openai-math-followups notes had reported this ‘numerically’ on 10 Oct). Its verdict: ‘Nothing we found disputes the claim’