Erdős problem 756 · problems.science

Let $A\subset \mathbb{R}^2$ be a set of $n$ points. Can there be $\gg n$ many distinct distances each of which occurs for more than $n$ many pairs from $A$ ?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/756.lean

Formal Conjectures

FormalConjectures/ErdosProblems/756.leanErdos756.erdos_7561 lineExact file

1True ↔ (fun n => ↑n) =O[Filter.atTop] fun n => ↑(Erdos756.maxRichDistances n)

SolvedStatement only, no proof

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:756
PLBY Lean proofsErdosProblems.Erdos756

Reported activity

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

Formalization
Erdős AI contributions wiki · 15 Mar, 2026
Machine
Aristotle
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