Skip to content

Erdős problem 959

How large can the difference between the largest and second-largest distance multiplicities be among nn planar points?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

959.lean

Retained formal statement2 of 2

A superlinear lower bound: there is a c>0c>0 with extremalGap(n)≥n1+c/log⁡log⁡n\text{extremalGap}(n)\geq n^{1 + c/\log\log n} for all large nn, so max⁡(f(d1)−f(d2))\max (f(d_1)-f(d_2)) grows faster than any linear function of nn. Determining the exact order remains open, which is erdos_959.

FormalConjectures/ErdosProblems/959.leanErdos959.erdos_959.lower_bound1 lineExact file
∃ c, 0 < c ∧ ∃ N, ∀ n ≥ N, ↑n ^ (1 + c / Real.log (Real.log ↑n)) ≤ ↑(Erdos959.extremalGap n)
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.