Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated


Claim. K. Borsuk, Drei Sätze über die n-dimensionale euklidische Sphäre, Fund. Math. 20 (1933), 177--190. Besides the antipodal theorems for which the paper is known, it proves the planar case of the covering question it poses: every bounded set of diameter 11 in R2\mathbb R^2 is the union of three sets of diameter <1<1. This is the instance n=2n=2 of the question, answered yes. The instance n=1n=1 is elementary, the instance n=3n=3 is Eggleston's, and the question is answered no in general by the full claims recorded on this problem's other pages. The page is dated to the publication year, the record giving no day.

Covers. The instance n=2n=2 of the question. The site calls the plane case easy and credits no source for it. The formal-conjectures statement files credit this paper with the plane case: at the commit of 2026-10-07, 505.lean states the assertion for n≤3n\le3 as a solved variant (erdos_505.small_dim) crediting Borsuk for n=2n=2, and the file it points to, BorsukConjecture.lean, states the plane case as borsuk_conjecture.two. Both are statement files, not formalization links. The second attaches as its formal proof a Lean development in a fork of that repository, which proves the plane case through Jung's inequality rather than by Borsuk's argument; this corpus has not built it, so it gives no formalized evidence here.

Depends on. No page of this wiki.

Acceptance. The result is refereed: Fundamenta Mathematicae published the paper. The site's label, DISPROVED (LEAN), credits Kahn and Kalai and Jenrich and Brouwer with the disproof and names no source for the plane, so no curator credit is recorded for this partial claim.