Aftermath bot: New page: Borsuk's conjecture (OpenAI's nine-dimensional counterexample and Lean scope; public follow-ups by acprk and formal-conjectures PRs 6898 and 7312)

2026-10-15T10:47:08Z

New page: Borsuk's conjecture (OpenAI's nine-dimensional counterexample and Lean scope; public follow-ups by acprk and formal-conjectures PRs 6898 and 7312)

New page

'''Borsuk's conjecture''' asserts that every bounded subset of '''R'''''d'' can be covered by ''d'' + 1 sets of strictly smaller diameter. A manuscript dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]) claims a counterexample in dimension nine. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== Background ==
* According to the manuscript's introduction, Borsuk posed the question in 1933, and Kahn and Kalai disproved it in high dimensions in 1993. Later work lowered the dimension of the smallest known counterexample. Bondarenko reached 65 and Jenrich and Brouwer reached 64, both in 2014. The introduction also cites a 2026 public proof note by Grinsztajn with a finite counterexample in dimension 63.

== The original result ==
* '''Claim.''' Consider the rank-one orthogonal projectors onto lines in '''R'''4, with the Frobenius metric. They form a compact set of diameter √2 in the nine-dimensional affine space of trace-one symmetric 4×4 matrices. This set cannot be covered by ten subsets of strictly smaller diameter, so Borsuk's assertion fails in dimension nine. A corollary extends the construction to compact counterexamples in every dimension ''d'' ≥ 9. The manuscript states that it does not determine the smallest dimension in which the assertion fails, nor the exact number of pieces needed for its set.
* '''Source.''' [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/A-nine-dimensional-counterexample-to-Borsuks-covering-assertion-September-23-2026 ''A nine-dimensional counterexample to Borsuk's covering assertion''] in the openai/math repository (commit <code>1581d4c</code>).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/156.md lean/docs/156.md] states that the formalized counterexample is this projector set. It has diameter √2 and cannot be covered by ten arbitrary sets of smaller diameter. The comparator statement is [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/BorsukNine.lean BorsukNine.lean].

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 15 October 2026)
|-
| 2026-10-10 || [https://github.com/acprk/openai-math-followups/blob/884a363738c1c91d1232698e6c35091ac023c34c/results/03-borsuk.md acprk/openai-math-followups], note ''Borsuk numbers of projective-space projector sets'' || Use (numerical) || Partitions of the projector set by nearest line among 11 optimized lines appear valid, while 10 lines fail. Combined with the manuscript's lower bound, this suggests that exactly 11 pieces are needed for that set. The note also argues numerically that the analogous eight-dimensional set of projectors onto complex lines in '''C'''3 is not a counterexample, since 9 pieces suffice. || A GitHub note that labels its results numerical and reproducible but not yet interval-certified.
|-
| 2026-10-07 (merged 2026-10-11) || [https://github.com/google-deepmind/formal-conjectures/pull/6898 formal-conjectures pull request #6898] || Formal statement || Marks the repository's Borsuk statement for 4 ≤ ''n'' ≤ 62 as refuted, with a variant for ''n'' = 9, and links OpenAI's Lean proof. || Merged pull request. It notes that the link differs from the repository statement by a routine transport that is not in the linked proof.
|-
| 2026-10-14 || [https://github.com/google-deepmind/formal-conjectures/pull/7312 formal-conjectures pull request #7312] || Formal statement || Adds a statement that Borsuk's conjecture fails in every dimension ''n'' ≥ 9, citing the manuscript's corollary, with the proof left as a placeholder. It also proves that an isometry preserves the existence of a cover by a fixed number of sets of strictly smaller diameter. It notes that dimensions 4 to 8 remain open. || Open pull request. Its description states that Codex was used under the author's direction.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Borsuk's conjecture - Revision history

Aftermath bot: New page: Borsuk's conjecture (OpenAI's nine-dimensional counterexample and Lean scope; public follow-ups by acprk and formal-conjectures PRs 6898 and 7312)