Problem 1071

../

claims/: The 3 claim pages of Problem 1071, one per claimant's result; the problem's standing derives from them.

---

Statement. Is there a finite set of unit line segments (rotated and translated copies of $(0,1)$) in the unit square, no two of which intersect, which are maximal with respect to this property?

Is there a region $R$ with a maximal set of disjoint unit line segments that is countably infinite?

Status. PROVED (LEAN): the site labels the problem PROVED (LEAN). The first question was answered yes by Danzer at the 1985 Siófok meeting, as Erdős reports, and the second by Boris Alexeev in the site's comments (January 2026) with the unit square as the region; see the claim pages of Danzer and Alexeev. Erdős's paper gives a second finite example for the first question, its Figure 4, found by a participant of the meeting whom he does not name; it has no claim page of its own because its claimant is unnamed. Alexeev's repository holds Lean proofs of both questions: the proof of the second is his own construction formalized, linked on his page, and the proof of the first formalizes the Figure 4 example and is recorded as an independent claim on its own page.

Source. erdosproblems.com/1071, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #1071, https://www.erdosproblems.com/1071.

References.

• [Er87b] Erdős, P., Some combinatorial and metric problems in geometry. Intuitive geometry (Siófok, 1985) (1987), 167-177.

Formalization. Statement in formal-conjectures. Boris Alexeev's repository of Lean proofs proves both questions. This corpus built its proof of the first, the theorem Erdos1071b.erdos_1071_finite, at a pinned commit of 2026-09-15, checked its axioms and its comparator challenge, and audited its statement against the Statement, so its claim page lists formalized evidence; the Lean proof of the second question is linked on [[problems/discrete_geometry/E1071/claims/2026_01_25_alexeev|Alexeev's claim page]] and carries no formalized evidence.

Progress

Not yet compiled.

Known Results

Not yet compiled.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

• erdos_1987_combinatorial_metric_problems_geometry
• erdos_1987_combinatorial_metric_problems_geometry / question_p173