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 statement2 of 2

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.

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

FormalConjectures/ErdosProblems/1071.leanErdos1071.erdos_1071.parts.ii10 linesExact file

1True ↔2  ∃ R S,3    IsOpen R ∧4      IsConnected R ∧5        S.Countable ∧6          S.Infinite ∧7            Maximal8              (fun T =>9                (∀ seg ∈ T, dist seg.1 seg.2 = 1 ∧ seg.1 ∈ R ∧ seg.2 ∈ R) ∧ 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