Erdős problem 959
How large can the difference between the largest and second-largest distance multiplicities be among planar points?
Sources
FormalConjectures/ErdosProblems/
959.lean
Retained formal statement
Let be a set of size and let be the set of distinct distances determined by . Let be the number of times the distance is determined, ordered so that . Estimate where the maximum is taken over all of size (this is extremalGap n).
The asymptotic order of extremalGap is not known; a natural formalization of "estimate" asks whether it has a well-defined polynomial growth exponent.
True ↔ ∃ γ, Filter.Tendsto (fun n => Real.log ↑(Erdos959.extremalGap n) / Real.log ↑n) Filter.atTop (nhds γ)OpenStatement only, no proof