---

Claim. The answer to the first question of Problem 1071 is yes: the closed unit square holds a finite maximal family of pairwise disjoint open unit segments. Boris Alexeev's repository of Lean proofs of Erdős problems proves it as the theorem Erdos1071b.erdos_1071_finite of the file src/latest/ErdosProblems/Erdos1071.lean (line 8844 at the first pinned commit above), which keeps the original name erdos_1071b as an alias; that file merges this construction with the countable construction of the second question. The file first posted on 2026-02-13, Erdos1071b.lean (the second link above), proves the same statement under the name erdos_1071b. Five explicit segments do it in the open square (S_finite), and the four sides added to them do it in the closed square (S_total). The five segments are the two unit segments from the corner $(0,0)$ to $(\cos15^\circ,\sin15^\circ)$ and to $(\sin15^\circ,\cos15^\circ)$, which leave the corner at $15^\circ$ to the two adjacent sides and form an equilateral triangle with the unit segment joining their far ends, and two near-side unit segments, one from $(x_1,0)$ to $(1,y_1)$ along the right side and its mirror image in the diagonal along the top side, each passing through the vertex of the triangle on its side; here $x_1\approx0.954$ is a root of a polynomial of degree $16$ and $y_1$ is determined by the unit length. Up to a symmetry of the square this is the second example of Erdős's 1987 problem paper (card, Section 7, Figure 4, p. 174), the one he attributes to a participant of the 1985 Siófok meeting whom he does not name, and not Danzer's Figure 3, which has a V from the two upper corners; the proof of maximality is the file's, since the paper gives the figure alone.

Submission note. Posted to the site's forum by Boris Alexeev on 13 February 2026:

Aristotle has formalized the solution to the first part also. It took 25 runs over 2 weeks, and the code is over 5000 lines! (All of those metrics are significantly more than usual.) Type-check it online!

(The site has been updated to address this comment.)

Covers. The first question only: a finite maximal family of pairwise disjoint open unit segments exists in the closed unit square, which answers the first question yes; the closed-square and open-square readings of the question are equivalent. The second question is settled on Alexeev's claim page, and the first was first answered by Danzer, whose example is recorded on Danzer's claim page.

Depends on. No page of this wiki.

Claimant. Boris Alexeev published Erdos1071b.lean in their repository and reported it in the problem's thread on 2026-02-13, saying that Aristotle (Harmonic) had formalized the solution to the first part in twenty-five runs over two weeks and more than five thousand lines. That file's header names no informal author and declares itself a formalization of no one's result, so it is recorded as an independent proof with its own page rather than as a link on Danzer's. The merged file's header names Everett Howe and Boris Alexeev as informal authors and Aristotle, ChatGPT and Boris Alexeev as formal authors, and the authors key lists those formal authors; the header's summary describes the countable construction (its Corollary 3), and the section that holds this construction has no author block of its own. Neither file contains sorry. The formal-conjectures statement file attaches the original file to its second question, the countable family, while its docstring for the first question credits Danzer and attaches the Lean proof of the countable construction; the two addresses are swapped.

Acceptance. Formalized. This corpus's verification built the module ErdosProblems.Erdos1071 and the comparator challenge Erdos1071 from the repository at its pinned commit of 2026-09-15, the first link above (Lean v4.33.0, Mathlib v4.33.0, the toolchain of its src/latest folder), which holds the merged file, a later revision of the file posted on 2026-02-13; the build is of that revision, not of the posted one. It checked the axioms of Erdos1071b.erdos_1071_finite, which are exactly propext, Classical.choice and Quot.sound. The repository's comparator challenge for the problem pins that declaration together with the definitions its type reaches (the point type, unit segments, disjoint collections, containment in a region, maximal disjoint collections and the closed unit square), and the fingerprint of the compiled declaration was found identical to the challenge; the solution's definitions and statement are the challenge's. The statement was audited clause by clause against the problem's Statement and is exact: it asserts a finite family of open Euclidean unit segments (open segments whose endpoints are at distance $1$) lying in the closed unit square, with distinct members disjoint, that is maximal against every disjoint family in the square containing it; the empty family is not maximal, so the condition is not met vacuously. The closed-square reading is equivalent to the open-square one: an open unit segment in $[0,1]^2$ that meets the boundary is a side, so every maximal family in the closed square contains the four sides and the rest of it is maximal in the open square, and the converse also holds. The compared statement is the closed-square one; the open-square result for the five segments alone (S_finite) is proved in the file but no challenge compares it. Not reviewed: the site labels the problem PROVED (LEAN), but Thomas Bloom, its curator, credits the first question to Danzer, not to this file, and no outside reviewer has published an examination of it. Not refereed: the proof has no journal publication.