Erdős problem 959 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

959.lean

Retained formal statement2 of 2

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

FormalConjectures/ErdosProblems/959.leanErdos959.erdos_959.lower_bound1 lineExact file

1∃ 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.

Sources

Search problems.science