Erdős problem 659 · problems.science

Is there a set of $n$ points in $\mathbb{R}^2$ such that every subset of $4$ points determines at least $3$ distances, yet the total number of distinct distances is $\ll \frac{n}{\sqrt{\log n}}$ ?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/659.lean

Formal Conjectures

FormalConjectures/ErdosProblems/659.leanErdos659.erdos_6594 linesExact file

1True ↔2  ∃ A,3    (∀ (n : ℕ), (A n).card = n ∧ ∀ S ⊆ A n, S.card = 4 → 3 ≤ EuclideanGeometry.distinctDistances S) ∧4      (fun n => ↑(EuclideanGeometry.distinctDistances (A n))) =O[Filter.atTop] fun n => ↑n / √(Real.log ↑n)

SolvedStatement only, no proof

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:659
PLBY Lean proofsErdosProblems.Erdos659

Reported activity

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

AI alongside literature
Erdős AI contributions wiki · 2 Feb, 2026
Machine
Aletheia
Open the source record
Formalization
Erdős AI contributions wiki · 14 Jan, 2026
Machine
Aristotle
Open the source record
AI collaborating with humans
Erdős AI contributions wiki · 13 Jan, 2026
Machine
Gemini 3
People
Benjamin Grayzel
Open the source record
argument
VibeMathed
Machine
Gemini 3, Aletheia
People
Benjamin Grayzel
Reported outcome
resolved
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science