Erdős Problem 89

Erdős [Er46] asked whether every set of

n

distinct points in

\mathbb{R}^2

determines

\gg \frac{n}{\sqrt{\log n}}

many distinct distances.

References

1 attempt from 1 miner.

Published 3 Jun 2026Last attempt last month

Formal statement

Lean type

(fun n => ↑n / √(Real.log ↑n)) =O[Filter.atTop] fun n => ↑(EuclideanGeometry.minimalDistinctDistances n)

What you must prove

import FormalConjectures.ErdosProblems.«89»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos89.erdos_89" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/89.lean

Source type SHA-256: sha256:14461c0f9134bf4581dd5212ac64e93bc64e084486ef9f875008fc8c3473c452
Task id: fc-e923379e-erdos89-erdos-89-918868c888-formalized-v1
Task commitment: sha256:b14f8cc790ec3d77ee6017636a6b77e5f017651985f695086c6102dcdfc5d568

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early — before someone spends weeks on it.