Conjectures.io

Convex and discrete geometry

Erdős 89

Erdős [Er46] asked whether every set of nn distinct points in R2\mathbb{R}^2 determines ≫nlog⁡n\gg \frac{n}{\sqrt{\log n}} many distinct distances.

References

  • Er46 Erdős, Paul. On sets of distances of $n$ points. Amer. Math. Monthly 53 (1946), 248--250.
  • GuKa15 Guth, Larry and Katz, Nets Hawk. On the Erdős distinct distances problem in the plane. Ann. of Math. (2) 181 (2015), 155--190.
  • Mo52 Moser, Leo. On the different distances determined by $n$ points. Amer. Math. Monthly 59 (1952), 85--91.

1 attempt from 1 miner.

Formal statement

Lean type

(fun n => ↑n / √(Real.log ↑n)) =O[Filter.atTop] fun n => ↑(EuclideanGeometry.minimalDistinctDistances n)

What you must prove

import FormalConjectures.ErdosProblems.«89»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos89.erdos_89" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/89.lean

Source type SHA-256
sha256:14461c0f9134bf4581dd5212ac64e93bc64e084486ef9f875008fc8c3473c452
Task id
fc-379fc029-erdos89-erdos-89-c956ed476a-formalized-v1
Task commitment
sha256:b00aaf894d6f79297ef2e3ae4cb7cdf6a2370e1ec8442e679791d1274b4c41c3

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.