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 in is the union of three sets of diameter . This is the instance of the question, answered yes. The instance is elementary, the instance 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 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 as a solved variant (erdos_505.small_dim)
crediting Borsuk for , 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.