Skip to content

Erdős problem 1071

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.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/1071.lean

Formal Conjectures

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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:1071
  • PLBY Lean proofsErdosProblems.Erdos1071

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

  • Formalization

    Erdős AI contributions wiki · 29 Jan, 2026 (second part); 12 Feb, 2026 (first part)

    Machine
    Aleph Prover, Aristotle, GPT
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page