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

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.

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

FormalConjectures/ErdosProblems/1071.leanErdos1071.erdos_1071.parts.ii10 linesExact file
True ↔  ∃ R S,    IsOpen R ∧      IsConnected R ∧        S.Countable ∧          S.Infinite ∧            Maximal              (fun T =>                (∀ seg ∈ T, dist seg.1 seg.2 = 1 ∧ seg.1 ∈ R ∧ seg.2 ∈ R) ∧ 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.