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](https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-proof.pdf) 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