BorsukConjecture.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

14 declarations, 12 contain sorry, 0 declared as axioms

Borsuk's conjecture

In 1933 Karol Borsuk [Bo33] asked whether every bounded subset of $\mathbb{R}^n$ can be partitioned into $n + 1$ sets, each of strictly smaller diameter. The hypothesis that the answer is positive became known as Borsuk's conjecture.

The conjecture is true for $n = 2$ [Bo33] and $n = 3$ [Pe47, Eg55]. It is false in general: Kahn and Kalai [KK93] disproved it for $n = 1325$ and for all $n > 2014$. Bondarenko [Bo14] gave a counterexample in dimension $65$, and Jenrich and Brouwer [JB14] one in dimension $64$, the smallest refereed counterexample. In 2026 Grinsztajn [Gr26] posted a 321-point counterexample in dimension $63$, obtained with AI assistance and verified by exact computation; the same configuration was found independently by Konz and by Ji [Ji26]. The cases $4 \leq n \leq 62$ are open. In dimension $4$, every bounded set can be partitioned into $9$ parts of smaller diameter [La82], and a 2026 preprint reduces this to $8$ parts [TV26].

Erdős Problem 505 (FormalConjectures.ErdosProblems.«505») points to this file.

References:

Wikipedia
[Bo33] Borsuk, K. (1933). Drei Sätze über die n-dimensionale euklidische Sphäre. Fundamenta Mathematicae 20, 177–190. https://doi.org/10.4064/fm-20-1-177-190
[Pe47] Perkal, J. (1947). Sur la subdivision des ensembles en parties de diamètre inférieur. Colloquium Mathematicum 2, 45.
[Eg55] Eggleston, H. G. (1955). Covering a three-dimensional set with sets of smaller diameter. Journal of the London Mathematical Society 30, 11–24. https://doi.org/10.1112/jlms/s1-30.1.11
[La82] Lassak, M. (1982). An estimate concerning Borsuk partition problem. Bulletin of the Polish Academy of Sciences, Mathematics 30(9–10), 449–451.
[KK93] Kahn, J., Kalai, G. (1993). A counterexample to Borsuk's conjecture. Bulletin of the American Mathematical Society 29(1), 60–62. https://arxiv.org/abs/math/9307229
[Bo14] Bondarenko, A. (2014). On Borsuk's conjecture for two-distance sets. Discrete & Computational Geometry 51(3), 509–515. https://doi.org/10.1007/s00454-014-9579-4
[JB14] Jenrich, T., Brouwer, A. E. (2014). A 64-dimensional counterexample to Borsuk's conjecture. Electronic Journal of Combinatorics 21(4), P4.29. https://doi.org/10.37236/4069
[Gr26] Grinsztajn, M. (2026). A 63-dimensional counterexample to Borsuk's conjecture. Proof note and verification script, https://github.com/maaxgrin/borsuk-63-counterexample
[Ji26] Ji, Y. (2026). An AI generated counterexample to Borsuk problem in dimension 63. https://arxiv.org/abs/2608.12561 (withdrawn as a duplicate of [Gr26])
[TV26] Tolmachev, A., Voronov, V. (2026). Reducing the upper bound for the Borsuk number in $\mathbb{R}^4$ to 8. https://arxiv.org/abs/2605.19068
[OP28a] Tao, T. et al., Optimization problems, constant 28a (smallest Borsuk counterexample dimension). https://teorth.github.io/optimizationproblems/constants/28a.html
[Ka15] Kalai, G. (2015). Some old and new problems in combinatorial geometry I: Around Borsuk's problem. https://arxiv.org/abs/1505.04952

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/ErdosProblems/505.lean

def Borsuk.HasBorsukCover HasBorsukCover k s means that the set s can be covered by k sets, each of strictly smaller extended diameter than s line 88 source
Source documentation
HasBorsukCover k s means that the set s can be covered by k sets, each of strictly smaller extended diameter than s.
We use the extended diameter Metric.ediam rather than Metric.diam: the latter takes the junk value 0 on unbounded sets, which would make Set.univ a covering set of "small" diameter. With Metric.ediam, a set of diameter 0 has no Borsuk cover, and an unbounded set has no finite Borsuk cover, matching Borsuk's formulation for bounded sets with at least two points.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoEMetricSpace, Nat, Set
Proof uses: Exists, Fin, And, LE.le, Set.iUnion, LT.lt, ENNReal, Metric.ediam
4 instances, coercions and auxiliary constants left out.
```
def HasBorsukCover (k : ℕ) (s : Set E) : Prop :=
…
```
def Borsuk.BorsukConjecture Borsuk's conjecture in dimension n: every bounded subset of $\mathbb{R}^n$ with at least two points can be partitioned into $n + 1$ sets of strictly smaller diameter line 95 source
Source documentation
Borsuk's conjecture in dimension n: every bounded subset of $\mathbb{R}^n$ with at least two points can be partitioned into $n + 1$ sets of strictly smaller diameter.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Set, EuclideanSpace, Real, Fin, Bornology.IsBounded, OfNat.ofNat, ENNReal, Set.Nontrivial, Borsuk.HasBorsukCover, HAdd.hAdd
17 instances, coercions and auxiliary constants left out.
```
def BorsukConjecture (n : ℕ) : Prop :=
…
```
theorem Borsuk.borsuk_conjecture Documented declaration: borsuk_conjecture sorry line 106 source
Source documentation
Borsuk's conjecture, open range: every bounded subset of $\mathbb{R}^n$ with at least two points can be partitioned into $n + 1$ sets of strictly smaller diameter, for $4 \leq n \leq 62$.
The conjecture is known to be true for $n \leq 3$ and false for $n \geq 63$.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Borsuk.BorsukConjecture
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem borsuk_conjecture (n : ℕ) (hn : 4 ≤ n) (hn' : n ≤ 62) : BorsukConjecture n := by
…
```
Mentions: Borsuk.BorsukConjecture
theorem Borsuk.borsuk_conjecture.four Borsuk's conjecture in dimension $4$, the smallest open case sorry line 111 source
Source documentation
Borsuk's conjecture in dimension $4$, the smallest open case.

depends on sorry what this means
Statement uses: Borsuk.BorsukConjecture, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem borsuk_conjecture.four : BorsukConjecture 4 := by
…
```
Mentions: Borsuk.BorsukConjecture
theorem Borsuk.borsuk_conjecture.four.nine_parts Partial result in dimension $4$: every bounded subset of $\mathbb{R}^4$ with at least two points can be partitioned into $9$ sets of strictly smaller diameter sorry line 120 source
Source documentation
Partial result in dimension $4$: every bounded subset of $\mathbb{R}^4$ with at least two points can be partitioned into $9$ sets of strictly smaller diameter. Proved by Lassak [La82], who showed more generally that $2^{n-1} + 1$ parts suffice in $\mathbb{R}^n$.

depends on sorry what this means
Statement uses: Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Bornology.IsBounded, ENNReal, Set.Nontrivial, Borsuk.HasBorsukCover
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem borsuk_conjecture.four.nine_parts (s : Set (ℝ^4)) (hs : IsBounded s)
    (hs' : s.Nontrivial) : HasBorsukCover 9 s := by
…
```
Mentions: Borsuk.HasBorsukCover
theorem Borsuk.borsuk_conjecture.four.eight_parts Partial result in dimension $4$: every bounded subset of $\mathbb{R}^4$ with at least two points can be partitioned into $8$ sets of strictly smaller diameter sorry line 131 source
Source documentation
Partial result in dimension $4$: every bounded subset of $\mathbb{R}^4$ with at least two points can be partitioned into $8$ sets of strictly smaller diameter. Claimed by Tolmachev and Voronov [TV26] via computer-assisted partitions of a truncated Lassak cover, with floating-point verification; the preprint is not yet refereed.

depends on sorry what this means
Statement uses: Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Bornology.IsBounded, ENNReal, Set.Nontrivial, Borsuk.HasBorsukCover
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem borsuk_conjecture.four.eight_parts (s : Set (ℝ^4)) (hs : IsBounded s)
    (hs' : s.Nontrivial) : HasBorsukCover 8 s := by
…
```
Mentions: Borsuk.HasBorsukCover
theorem Borsuk.borsuk_conjecture.zero sorry line 139 source
depends on sorry what this means
Statement uses: Borsuk.BorsukConjecture, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Borsuk.borsuk_conjecture.one sorry line 149 source
depends on sorry what this means
Statement uses: Borsuk.BorsukConjecture, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Borsuk.borsuk_conjecture.two sorry line 156 source
depends on sorry what this means
Statement uses: Borsuk.BorsukConjecture, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Borsuk.borsuk_conjecture.three sorry line 163 source
depends on sorry what this means
Statement uses: Borsuk.BorsukConjecture, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Borsuk.borsuk_conjecture.not_forall sorry line 173 source
depends on sorry what this means
Statement uses: Not, Nat, Borsuk.BorsukConjecture
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Borsuk.borsuk_conjecture.not_sixty_five sorry line 180 source
depends on sorry what this means
Statement uses: Not, Borsuk.BorsukConjecture, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Borsuk.borsuk_conjecture.not_sixty_four sorry line 190 source
depends on sorry what this means
Statement uses: Not, Borsuk.BorsukConjecture, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Borsuk.borsuk_conjecture.not_sixty_three sorry line 201 source
depends on sorry what this means
Statement uses: Not, Borsuk.BorsukConjecture, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.