Claims

../

1987_01_01_danzer: A finite family of pairwise disjoint unit segments in the unit square to which no further unit segment can be added, found by Danzer at the 1985 Siófok meeting and reported by Erdős; answers the first question yes.

2026_01_25_alexeev: A countably infinite family of pairwise disjoint unit segments in the unit square to which no further unit segment can be added, posted in the site's comments and proved in Lean; answers the second question yes.

2026_02_13_alexeev: A Lean proof, formalized by Aristotle and posted by Boris Alexeev, that five unit segments and the four sides form a finite maximal disjoint family in the unit square (Erdős's second 1987 example); built and audited here.

---