Erdős problem 214

Let $S\subset \mathbb{R}^2$ be such that no two points in $S$ are distance $1$ apart. Must the complement of $S$ contain four points which form a unit square?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/214.lean

Formal Conjectures

FormalConjectures/ErdosProblems/214.leanErdos214.erdos_2143 linesExact file

1True ↔2  ∀ (S : Set (EuclideanSpace ℝ (Fin 2))),3    Erdos214.UnitDistanceAvoiding S → ∃ p, (∀ (i : Fin 4), p i ∈ Sᶜ) ∧ Congruent p Erdos214.unitSquare

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:214
PLBY Lean proofsErdosProblems.Erdos214

Reported activity

Reported by these sources. Not reviewed here.

Formalization
Erdős AI contributions wiki · 2 Mar, 2026
Machine
Aristotle
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry