Erdős problem 1071 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

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

1True ↔2  ∃ S,3    Maximal4      (fun T =>5        (∀ seg ∈ T,6            dist seg.1 seg.2 = 1 ∧7              seg.1.ofLp 0 ∈ Set.Icc 0 1 ∧8                seg.1.ofLp 1 ∈ Set.Icc 0 1 ∧ seg.2.ofLp 0 ∈ Set.Icc 0 1 ∧ seg.2.ofLp 1 ∈ Set.Icc 0 1) ∧9          (↑T).Pairwise Erdos1071.SegmentsDisjoint)10      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.

Sources

Search problems.science