Erdős problem 90
Conjectured upper bound on how many pairs among points in the plane can be exactly one unit apart.
Sources
FormalConjectures/ErdosProblems/
90.lean
Retained formal statement
Does every set of distinct points in contain at most many pairs which are distance apart?
This was disproved by an internal model at OpenAI, which constructed (for infinitely many ) a set of points in such that the number of unit distance pairs in is at least , where is an absolute constant.
False ↔ ∃ O, ∃ (_ : O =O[Filter.atTop] fun n => 1 / Real.log (Real.log ↑n)), (fun n => ↑(Erdos90.maxUnitDistances n)) =ᶠ[Filter.atTop] fun n => ↑n ^ (1 + O n)SolvedStatement only, no proof