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?

AMS 52 · solved (literature)

theorem erdos_1071.parts.i :
    answer(True) ↔ ∃ S : Finset (ℝ² × ℝ²),
      Maximal (fun T : Finset (ℝ² × ℝ²) =>
        (∀ seg ∈ T, dist seg.1 seg.2 = 1 ∧
          seg.1 0 ∈ Icc 0 1 ∧ seg.1 1 ∈ Icc 0 1 ∧
          seg.2 0 ∈ Icc 0 1 ∧ seg.2 1 ∈ Icc 0 1) ∧
          (T : Set (ℝ² × ℝ²)).Pairwise SegmentsDisjoint) S