Skip to content

Erdős problem 1071

Start work

Is there a region RR with a maximal set of disjoint unit line segments that is countably infinite? Solved affirmatively by [Fo99], who gave an explicit construction.

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1071.lean

Retained formal statement1 of 2

Can a finite set of disjoint unit segments in a unit square be maximal? Solved affirmatively by [Da85], who gave an explicit construction.

This was formalized in Lean by Alexeev using Aristotle and ChatGPT.

FormalConjectures/ErdosProblems/1071.leanErdos1071.erdos_1071.parts.i10 linesExact file
True ↔  ∃ S,    Maximal      (fun T =>        (∀ seg ∈ T,            dist seg.1 seg.2 = 1 ∧              seg.1.ofLp 0 ∈ Set.Icc 0 1 ∧                seg.1.ofLp 1 ∈ Set.Icc 0 1 ∧ seg.2.ofLp 0 ∈ Set.Icc 0 1 ∧ seg.2.ofLp 1 ∈ Set.Icc 0 1) ∧          (↑T).Pairwise Erdos1071.SegmentsDisjoint)      S
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.