Erdős Problem a Daythe open tracker
The board / geometry / #505

Erdős Problem #505
Borsuk's problem

DISPROVED LEANdatabase updated 2026-02-02

The statement as posed is false. A solution has also been checked by machine, in Lean.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

**Erdős Problem 505** (disproved). Borsuk's conjecture is false for sufficiently large \(n\): there exists a dimension \(n\) and a bounded set \(S \subseteq \mathbb{R}^n\) with at least two points that cannot be covered by \(n + 1\) subsets each of strictly smaller diameter. Erdős [Er44] suspected this. Disproved by Kahn–Kalai [KK93] for \(n \geq 2015\). Currently known to be false for \(n = 9\) [OAI26] and for \(n \geq 63\). A formal proof was formalised by Boris Alexeev using Aristotle.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/505.
Newer public claim (6 Oct 2026): OpenAI's internal-model release claims, for this problem, a Borsuk counterexample in dimension 9 (record was 64, then 63) — refereed here 20 Oct; OpenAI's Lean (269 modules) kernel-replayed on our machine, statement matched; eleven pieces do cover its set (our exact certificate), so its Borsuk number is exactly 11 — see /day/505-openai-borsuk-fails-in-dimension-nine-refereed — family 156 at github.com/openai/math, OpenAI's own Lean proves Theorem 1.1 (no ten sets of diameter < √2 cover the projectors onto lines in ℝ⁴) and its ℝ⁹ form — kernel-replayed on our machine on 20 Oct 2026 (269 modules, 0 errors, standard axioms, statement matched to the comparator challenge under pp.all, leanchecker --fresh over the whole closure rc 0); a kernel-checked bridge of ours derives Formal Conjectures' borsuk_conjecture.not_nine and erdos_505 statements from it — see our /day entry. Bloom calls these claims, not endorsements.
Prizenone
Topicsgeometry
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/505

Attempts

submit one →
FULL WRITE-UP BY THIS SITE · OCT 20, 2026

Read our full write-up →

Borsuk asked in 1933 (Erdős #505) whether every set of diameter 1 in ℝⁿ is a union of n + 1 sets of smaller diameter. Kahn and Kalai answered no in 1993 for every n > 2014. Since then the smallest known failing dimension has come down to 64 (Jenrich–Brouwer 2014; the problem page still says 64) and then to 63 (Grinsztajn 2026, a finite set). OpenAI's 6 October release claims nine. Its set is X = {uuᵀ : u a unit vector in ℝ⁴}, which lies in the nine-dimensional space of trace-one symmetric 4×4 matrices; no ten sets of diameter below √2 cover it. The construction is Kalai's: he proposed the projector sets of ℝⁿ as candidate counterexamples in 2011 and 2015, for n large enough to reach dimensions above about 70. OpenAI's Lean proof (269 modules) replays on our machine with the standard axioms, and its statement matches OpenAI's comparator challenge. Three AI referee seats and our own reading of §§5–6 found only exposition problems in the paper. The kernel-checked proof takes a different route from the printed one in its degree theory and in most of the finite step, so the replay and the reading each check something the other does not. For covers by caps the result already follows from Walkup's 1970 bound on triangulations of ℝP³, so the new step is arbitrary sets. Ours: an exact certificate that eleven sets do cover X, which with OpenAI's theorem makes its Borsuk number exactly 11 (reported numerically, without a certificate, on 10 October); an independent SAT check of the finite step with a verified certificate, which shows the step needs less than the paper uses; and a kernel-checked bridge to the statement in Formal Conjectures, whose current link proves a differently worded theorem. The problem itself was answered no in 1993.

CLOSED
← #504the board#506 →