Skip to content

Erdős problem 90

Conjectured upper bound on how many pairs among nn points in the plane can be exactly one unit apart.

Sources

The source's own material, retained exactly.

9 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

90.lean

Retained formal statement6 of 8

Sawin's Lemma 2: lattice geometry of unit distances (Sawin, arXiv:2605.20579).

Let d≥1d \ge 1, R≥2R \ge 2, and suppose Λ⊂R2d\Lambda \subset \mathbb{R}^{2d} is a lattice equipped with an additive embedding π:Λ→R2\pi : \Lambda \to \mathbb{R}^2. Suppose S⊆ΛS \subseteq \Lambda is a finite set of "matching" vectors satisfying ∥v∥≤1\|v\| \le 1 and ∥πv∥=1\|\pi v\| = 1 for every v∈Sv \in S. Then there is a finite point set U⊂R2U \subset \mathbb{R}^2 with unit-distance density at least (1−1/R)2d #S(1 - 1/R)^{2d}\,\#S, i.e. (1−1/R)2d #S #U≤#{unit pairs in U}(1-1/R)^{2d}\,\#S\,\#U \le \#\{\text{unit pairs in } U\}.

This pure geometry-of-numbers reduction is the elementary heart of the disproof.

FormalConjectures/ErdosProblems/90.leanErdos90.sawin_lattice_reduction12 linesExact file
∀ (d : ℕ),  1 ≤ d →    ∀ (R : ℝ),      2 ≤ R →        ∀ (Λ : Submodule ℤ (EuclideanSpace ℝ (Fin (2 * d)))) (π : ↥Λ →+ EuclideanSpace ℝ (Fin 2)),          Function.Injective ⇑π →            ∀ (S : Finset ↥Λ),              (∀ v ∈ S, ‖↑v‖ ≤ 1) →                (∀ v ∈ S, ‖π v‖ = 1) →                  ∃ U,                    0 < U.card ∧                      (1 - 1 / R) ^ (2 * d) * ↑S.card * ↑U.card ≤ ↑(EuclideanGeometry.unitDistancePairsCount U)
SolvedStatement only, no proof