---

Claim. The answer to the second question of Problem 1071 is yes, with the unit square itself as the region: there is a countably infinite family of pairwise disjoint unit segments in the unit square such that every further unit segment in the square meets one of them. The construction, posted in the problem's discussion, first cuts the square with a few segments, among them a unit segment from $(0,0)$ to $(\sqrt3/2,1/2)$ and symmetric copies of it, so that the only room left for a further unit segment lies in two thin parallelograms; in each, successive unit segments cut triangles off the current parallelogram and leave a smaller one, the nested parallelograms shrink to a shared diagonal, and a last unit segment on that diagonal completes the family, so the family is countably infinite while no unit segment fits anywhere else. The Lean file linked above states the result three times: for a region $R$ built for the purpose (its Theorem 1), for the open unit square (Corollary 2), and for the closed unit square with its four sides added to the family (Corollary 3).

Covers. The second question only: a region with a countably infinite maximal family of pairwise disjoint unit segments exists, and the unit square is one. The first question, a finite maximal family in the unit square, is settled on Danzer's claim page.

Claimant. Boris Alexeev posted the construction in the problem's discussion on 2026-01-25 and a Lean proof on 2026-01-30, in Alexeev's repository of Lean proofs of Erdős problems, linked above at a pinned commit. The file's header names Alexeev as the author of the proof, states that it was formalized by Aristotle (Harmonic), ChatGPT (OpenAI) and the author, and adds the author's doubt that the construction is new; it contains no sorry. The formal-conjectures statement file credits the second question to a reference it labels Fo99 without expanding it; the reference is unidentified. That file attaches Alexeev's proof of this question to its first question and the Lean proof of the first question, recorded on [[problems/discrete_geometry/E1071/claims/2026_02_13_alexeev|Alexeev's Lean page]], to its second.

Other claims of the result. The problem's thread holds an earlier independent sketch of the same construction. A forum user with the username "however" posted on 2026-02-11 that they had sketched a proof on Bluesky on 2026-01-03, and copied the sketch into the thread (post): cut the square at $x=1/2$, then nest parallelograms with vertices $(0,0)$ and $(1/2,1)$ that shrink to that diagonal, and finish with a unit segment on the diagonal. Thomas Bloom replied (post) that Bloom had missed the sketch and would update the remarks to credit it too; the site's remarks, last edited 2026-02-01, carry no such credit. The sketch is a thread post and not a manuscript, so it has no page of its own.

Acceptance. Thomas Bloom, the site's curator, labels the problem proved and records in the problem's commentary that Alexeev proved in the comments that the unit square admits a countably infinite maximal family (page last edited 2026-02-01); that credit is the reviewed evidence. This corpus's verification built a later revision of the Lean file, the merged file src/latest/ErdosProblems/Erdos1071.lean at the repository's commit of 2026-09-15 (Lean v4.33.0), linked on [[problems/discrete_geometry/E1071/claims/2026_02_13_alexeev|Alexeev's Lean page]], not the file posted on 2026-01-30. It found that the theorem Erdos1071.erdos_1071, the closed-square statement of Corollary 3, depends only on the axioms propext, Classical.choice and Quot.sound, and that its fingerprint is identical to the repository's comparator challenge. Its statement was not audited against the problem's Statement, so formalized is not listed, and there is no refereed write-up.

What remains. Erdős's further question, what happens when two segments may share an endpoint, is a variant outside the problem's statement and is not addressed by either claim page.