Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. The answer to the first question of Problem 1071 is yes: there is a finite family of pairwise disjoint unit segments in the unit square which is maximal, in that every further unit segment in the square meets one of them. Erdős reports in his 1987 problem paper (card, Section 7, pp. 173–174) that he and G. Fejes Tóth raised the question at the 1985 Siófok meeting, that Danzer found a simple example, drawn as the paper's Figure 3, which cost Erdős the $10 he had offered, and that another participant found a second example, Figure 4. Erdős adds that the positions of the segments can be varied in both examples, and asks what happens for other regions and when two segments may share an endpoint. The paper gives the figures without a written proof of maximality. The second example, whose author Erdős does not name, is the one proved in Lean on Alexeev's Lean page; no Lean proof of Danzer's own figure is recorded.
Covers. The first question only: a finite maximal family of pairwise disjoint unit segments in the unit square exists. The second question, a region with a countably infinite maximal family, is settled on Alexeev's claim page.
Claimant. The example is Danzer's; its only publication is Erdős's report in Intuitive geometry (Siófok, 1985), Colloq. Math. Soc. János Bolyai 48, North-Holland (1987), 167–177. The page is dated to the publication year because the record gives no day. The formal-conjectures statement file cites the example to a reference it labels Da85 with the title and pages of Erdős's paper, and its docstring for the first question credits Danzer and says that Alexeev formalized it; the Lean file it attaches to that question holds the countable construction of the second question, and the file it attaches to the second question holds the proof of the Figure 4 example recorded on [[problems/discrete_geometry/E1071/claims/2026_02_13_alexeev|Alexeev's Lean page]].
Acceptance. Erdős, who posed the question, accepted the example and paid the
prize, as his paper records. Thomas Bloom, the site's curator, labels the
problem proved and credits Danzer with the first question on the problem's page
at erdosproblems.com (page last edited 2026-02-01); that credit is the
reviewed evidence. No refereed proof of maximality is recorded.