Skip to content

Erdős problem 756

Start work

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

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
True ↔ (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

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry