Distinct and unit distances

DefinitionMultiplicity of a distance#✓fully proved

Let \(P\) be a finite set of points in a metric space and let \(d\) be a real number. The multiplicity of \(d\) in \(P\) is the number of unordered pairs \(\{p, q\}\) of distinct points of \(P\) with \(\operatorname{dist}(p, q) = d\).

noncomputable def distanceMultiplicity (points : Finset X) (d : ℝ) : ℕ :=
  #(points.offDiag.filter fun (pair : X × X) => dist pair.1 pair.2 = d) / 2

Used by 3

Used byRich distances · Number of unit distances · Trivial upper bound on unit distances

DefinitionNumber of unit distances#✓fully proved

For a finite set \(S\) of points in a metric space, the number of unit distances of \(S\) is the number of unordered pairs \(\{p, q\}\) of points of \(S\) with \(\operatorname{dist}(p, q) = 1\), that is, the multiplicity of the distance \(1\) in \(S\).

noncomputable def unitDistNum (s : Finset X) : ℕ := distanceMultiplicity s 1

Uses 1 · Used by 3

Statement usesMultiplicity of a distance

Used byUnit distance count of a planar point set · Number of unit-distance pairs in a planar point set · Trivial upper bound on unit distances

DefinitionDistance set of a finite point set#✓fully proved

For a finite set \(P\) of points in a metric space, the distance set of \(P\) is the finite set of real numbers \(\operatorname{dist}(p, q)\) with \(p\) and \(q\) distinct points of \(P\).

noncomputable def distanceSet (points : Finset X) : Finset ℝ :=
  points.offDiag.image fun (pair : X × X) => dist pair.1 pair.2

Used by 2

Used byNumber of distinct distances · Rich distances

DefinitionNumber of distinct distances#✓fully proved

For a finite set \(P\) of points in a metric space, the number of distinct distances of \(P\) is the number of elements of its distance set, that is, the number of distinct values \(\operatorname{dist}(p, q)\) with \(p\) and \(q\) distinct points of \(P\).

noncomputable def distinctDistances (points : Finset X) : ℕ :=
  #(distanceSet points)

Uses 1 · Used by 2

Statement usesDistance set of a finite point set

Used byStatement of Erdős Problem 659 · Minimum number of distinct distances

DefinitionMinimum number of distinct distances#✓fully proved

Let \(X\) be a metric space and \(n\) a natural number such that \(X\) contains a set of exactly \(n\) points. The minimum number of distinct distances for \(n\) points in \(X\) is the least number of distinct distances determined by a set of exactly \(n\) points of \(X\).

The hypothesis that some \(n\)-point set exists makes the minimum range over a nonempty collection of sets.

noncomputable def minimalDistinctDistances (n : ℕ) (_ : ∃ points : Finset X, #points = n) : ℕ :=
  sInf {m : ℕ | ∃ points : Finset X, #points = n ∧ distinctDistances points = m}

Uses 1

Statement usesNumber of distinct distances

DefinitionNumber of distinct distances from a point#✓fully proved

For a finite set \(P\) of points in a metric space and a point \(x\) of the space, this is the number of distinct values \(\operatorname{dist}(y, x)\) with \(y\) a point of \(P\) other than \(x\).

noncomputable def distinctDistancesFrom (points : Finset X) (pt : X) : ℕ :=
  #((points.erase pt).image fun x => dist x pt)

Used by 2

Used byMaximum number of distinct distance counts · Points with few distinct distances

TheoremTrivial upper bound on unit distances#✓fully proved

For a finite set of \(n\) points in a metric space, the number of unit distances is at most \(\binom{n}{2}\), the total number of unordered pairs of distinct points.

theorem unitDistNum_le_choose_two (s : Finset X) : unitDistNum s ≤ (#s).choose 2

Uses 2

Statement usesNumber of unit distances

Proof usesMultiplicity of a distance

DefinitionStatement of Erdős Problem 754#✓fully proved

This is the statement that there is a real constant \(C\) such that for every nonempty finite set \(A\) of points of the Euclidean space \(\mathbb{R}^4\) and every natural number \(f\), if for every \(x \in A\) there is a real number \(r > 0\) such that at least \(f\) points of \(A\) lie at distance \(r\) from \(x\), then \(f \le |A|/2 + C\). Equivalently, \(f(n) \le n/2 + O(1)\), where \(f(n)\) is the largest \(f\) such that some set \(A\) of \(n \ge 1\) points of \(\mathbb{R}^4\) has, for every \(x \in A\), at least \(f\) points of \(A\) at one common distance \(r(x) > 0\) from \(x\).

def favouriteDistanceCountHalfPlusConstant : Prop :=
  ∃ C : ℝ, ∀ (A : Finset (EuclideanSpace ℝ (Fin 4))) (f : ℕ), A.Nonempty →
    (∀ x ∈ A, ∃ r : ℝ, 0 < r ∧ f ≤ {y | y ∈ A ∧ dist x y = r}.ncard) →
      (f : ℝ) ≤ A.card / 2 + C

Used by 1

Used byErdős Problem 754: favourite distances in \(\mathbb{R}^4\)

TheoremErdős Problem 754: favourite distances in \(\mathbb{R}^4\)#●ready to prove

There is a real constant \(C\) such that for every nonempty finite set \(A\) of points of the Euclidean space \(\mathbb{R}^4\) and every natural number \(f\), if for every \(x \in A\) there is a real number \(r > 0\) such that at least \(f\) points of \(A\) lie at distance \(r\) from \(x\), then \(f \le |A|/2 + C\).

Swanepoel proved that for every finite \(A \subseteq \mathbb{R}^4\) with \(|A| = n\) and every choice of distances \(r(x) > 0\), the number of pairs \((x, y)\) of points of \(A\) with \(|x - y| = r(x)\) is at most \(n^2/2 + O(n)\), which gives this bound.

public theorem_wanted favouriteDistanceCountHalfPlusConstant_holds :
    favouriteDistanceCountHalfPlusConstant

Sources

• T. F. Bloom, Erdős Problems, Problem #754, https://www.erdosproblems.com/754 (status PROVED (LEAN)); resolution: K. J. Swanepoel, Favourite distances in high dimensions, Thirty Essays on Geometric Graph Theory (2013), 499-519, abstract of arXiv:1108.4817: f_d(n) = max ∑_{x ∈ S} e_r(x, S) = (1 - 1/⌊d/2⌋) n² + Θ(n) for even d (n²/2 + O(n) for d = 4); erdosproblems.com/754: proved by Swanepoel (Avis, Erdős and Pach had n/2 + 2 ≤ f(n) ≤ (1 + o(1)) n/2), https://arxiv.org/abs/1108.4817.

Uses 1

Statement usesStatement of Erdős Problem 754

DefinitionStatement of Erdős Problem 659#✓fully proved

This is the statement that there is a real constant \(C\) such that for every sufficiently large natural number \(n\) there is a set \(P\) of \(n\) points of the Euclidean plane \(\mathbb{R}^2\) such that every \(4\)-element subset of \(P\) determines at least \(3\) distinct distances and \(P\) determines at most \(C n / \sqrt{\log n}\) distinct distances.

def fewDistancesWithFourPointCondition : Prop :=
  ∃ C : ℝ, ∀ᶠ n : ℕ in Filter.atTop, ∃ P : Finset (EuclideanSpace ℝ (Fin 2)), P.card = n ∧
    (∀ S ⊆ P, S.card = 4 → 3 ≤ distinctDistances S) ∧
    (distinctDistances P : ℝ) ≤ C * n / Real.sqrt (Real.log n)

Uses 1 · Used by 1

Statement usesNumber of distinct distances

Used byErdős Problem 659: few distances with every four points spanning three

TheoremErdős Problem 659: few distances with every four points spanning three#●ready to prove

There is a real constant \(C\) such that for every sufficiently large natural number \(n\) there is a set \(P\) of \(n\) points of the Euclidean plane \(\mathbb{R}^2\) such that every \(4\)-element subset of \(P\) determines at least \(3\) distinct distances and \(P\) determines at most \(C n / \sqrt{\log n}\) distinct distances.

A suitable truncation of the lattice \(\{(a, b\sqrt{2}) : a, b \in \mathbb{Z}\}\) has \(O(n / \sqrt{\log n})\) distinct distances (Moree and Osburn) and contains none of the six four-point configurations that determine only two distances: five of them contain a square or an equilateral triangle (Erdős–Fishburn, Lund–Sheffer), and the pentagon configuration is excluded by Grayzel.

public theorem_wanted fewDistancesWithFourPointCondition_holds : fewDistancesWithFourPointCondition

Sources

• T. F. Bloom, Erdős Problems, Problem #659, https://www.erdosproblems.com/659 (status PROVED (LEAN)); resolution: B. Grayzel, Solution to a Problem of Erdős Concerning Distances and Points, arXiv:2601.09102 (2026); P. Moree and R. Osburn, Two-dimensional lattices with few distances, Enseign. Math. (2) 52 (2006), 361-380, abstract of arXiv:2601.09102: n-point sets taken from an m × m box of the lattice {(x, √2 y)} determine O(n / √(log n)) distinct distances (Bernays' theorem for u² + 2v²) and every 4 of their points determine at least 3 distances (Perucca's classification of the six two-distance 4-point configurations); erdosproblems.com/659 records the construction (Moree-Osburn, Lund-Sheffer) and the remaining pentagon case ruled out by Grayzel (using Gemini), 'thus giving a complete solution', https://arxiv.org/abs/2601.09102.

Uses 1

Statement usesStatement of Erdős Problem 659

DefinitionNumber of pairs at a given distance#✓fully proved

For a finite set \(P\) of points in \(\mathbb{R}^3\) and a real number \(\delta\), this is the number of unordered pairs \(\{p, q\}\) of distinct points \(p, q \in P\) with Euclidean distance \(|p - q| = \delta\), computed as half the number of ordered pairs \((p, q)\) of distinct points of \(P\) at distance \(\delta\) and taken as a real number.

noncomputable def pairsAtDistance (P : Finset (EuclideanSpace ℝ (Fin 3))) (δ : ℝ) : ℝ :=
  ((P.offDiag.filter fun pq => dist pq.1 pq.2 = δ).card : ℝ) / 2

Used by 1

Used byErdős Problem 605 (repeated distances on the sphere)

DefinitionErdős Problem 605 (repeated distances on the sphere)#✓fully proved

The proposition that there is a function \(f : \mathbb{N} \to \mathbb{R}\) with \(f(n) \to \infty\) as \(n \to \infty\) such that for every \(n \in \mathbb{N}\) there are a set \(P\) of \(n\) distinct points on the unit sphere \(\{x \in \mathbb{R}^3 : \|x\| = 1\}\) and a real number \(\delta\) for which the number of unordered pairs of distinct points of \(P\) at distance \(\delta\) is at least \(f(n) \cdot n\).

def sphereRepeatedDistanceSuperlinear : Prop :=
  ∃ f : ℕ → ℝ, Filter.Tendsto f Filter.atTop Filter.atTop ∧ ∀ n : ℕ,
    ∃ P : Finset (EuclideanSpace ℝ (Fin 3)), P.card = n ∧ (∀ p ∈ P, ‖p‖ = 1) ∧
      ∃ δ : ℝ, f n * n ≤ pairsAtDistance P δ

Uses 1 · Used by 1

Statement usesNumber of pairs at a given distance

Used byErdős Problem 605 is true

TheoremErdős Problem 605 is true#●ready to prove

There is a function \(f : \mathbb{N} \to \mathbb{R}\) with \(f(n) \to \infty\) as \(n \to \infty\) such that for every \(n \in \mathbb{N}\) there are a set \(P\) of \(n\) distinct points on the unit sphere \(\{x \in \mathbb{R}^3 : \|x\| = 1\}\) and a real number \(\delta\) for which the number of unordered pairs of distinct points of \(P\) at distance \(\delta\) is at least \(f(n) \cdot n\).

Erdős, Hickerson and Pach (Theorem 2(ii)) found an absolute constant \(c > 0\) such that for every \(n\) there are \(n\) points on the unit sphere each at distance \(\sqrt{2}\) from at least \(c n^{1/3}\) others, hence at least \(c n^{4/3} / 2\) pairs at distance \(\sqrt{2}\); erdosproblems.com/605 lists the problem as proved.

public theorem_wanted sphereRepeatedDistanceSuperlinear_holds : sphereRepeatedDistanceSuperlinear

Sources

• T. F. Bloom, Erdős Problems, Problem #605, https://www.erdosproblems.com/605 (status PROVED); resolution: P. Erdős, D. Hickerson and J. Pach, A problem of Leo Moser about repeated distances on the sphere, Amer. Math. Monthly (1989), 569-575, Theorem 2(ii): for every n there are n points on the unit sphere S² each at distance √2 from at least c₂ n^{1/3} others; Theorem 2(i): for every 0 < α < 2, n points each at distance α from at least c₁ log* n others, https://www.erdosproblems.com/605.

Uses 1

Statement usesErdős Problem 605 (repeated distances on the sphere)

AbbreviationUnit distance count of a planar point set#✓fully proved

For a finite set \(P\) of points in the Euclidean plane \(\mathbb{R}^2\), the unit distance count of \(P\) is the number of unordered pairs of points of \(P\) at distance exactly \(1\).

The distance is the Euclidean one, \(\sqrt{(x_1 - y_1)^2 + (x_2 - y_2)^2}\) for \(x = (x_1, x_2)\) and \(y = (y_1, y_2)\), not the largest coordinate difference used by the product metric on \(\mathbb{R} \times \mathbb{R}\).

noncomputable abbrev unitDist (P : Finset (EuclideanSpace ℝ (Fin 2))) : ℕ := unitDistNum P

Uses 1 · Used by 1

Statement usesNumber of unit distances

Used byErdős's unit distance conjecture is false

TheoremErdős's unit distance conjecture is false#●ready to prove

There is a real number \(\delta > 0\) such that for every natural number \(N\) there are an integer \(n \ge N\) and a set \(P\) of exactly \(n\) points in the Euclidean plane \(\mathbb{R}^2\) with at least \(n^{1+\delta}\) unordered pairs of points of \(P\) at distance exactly \(1\).

Because \(C / \log \log n \to 0\) for every constant \(C\), this contradicts Erdős's conjecture that \(n\) points in the plane determine at most \(n^{1 + C / \log \log n}\) unit distances for some constant \(C\) and all large \(n\).

public theorem_wanted erdos_unit_distance_conjecture_false :
    ∃ δ : ℝ, 0 < δ ∧
      ∀ N : ℕ, ∃ (n : ℕ) (P : Finset (EuclideanSpace ℝ (Fin 2))),
        N ≤ n ∧ P.card = n ∧ (n : ℝ) ^ (1 + δ) ≤ (unitDist P : ℝ)

Sources

• OpenAI, Planar Point Sets with Many Unit Distances, 2026. https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-proof.pdf . Original conjecture: P. Erdős, On sets of distances of n points, Amer. Math. Monthly 53 (1946), 248-250. k-equidistant variant: P. Erdős, K. Falconer, Some problems in combinatorial geometry, 1997. Problem erdos_unit_distance_conjecture_false of the lean-eval benchmark.

Uses 1

Statement usesUnit distance count of a planar point set

AbbreviationNumber of unit-distance pairs in a planar point set#✓fully proved

For a finite set \(P\) of points in the Euclidean plane \(\mathbb{R}^2\), the number of unit-distance pairs of \(P\) is the number of unordered pairs of points of \(P\) at distance exactly \(1\).

The distance is the Euclidean one, \(\sqrt{(x_1 - y_1)^2 + (x_2 - y_2)^2}\) for \(x = (x_1, x_2)\) and \(y = (y_1, y_2)\), not the largest coordinate difference used by the product metric on \(\mathbb{R} \times \mathbb{R}\).

noncomputable abbrev unitDist (P : Finset (EuclideanSpace ℝ (Fin 2))) : ℕ := unitDistNum P

Uses 1 · Used by 1

Statement usesNumber of unit distances

Used bySpencer–Szemerédi–Trotter unit distance bound

TheoremSpencer–Szemerédi–Trotter unit distance bound#●ready to prove

There is a constant \(C > 0\) such that every finite set of \(n\) points in the Euclidean plane \(\mathbb{R}^2\) has at most \(C n^{4/3}\) unordered pairs of points at distance exactly \(1\).

public theorem_wanted unit_distance_upper_bound :
    ∃ C : ℝ, 0 < C ∧
      ∀ P : Finset (EuclideanSpace ℝ (Fin 2)),
        (unitDist P : ℝ) ≤ C * (P.card : ℝ) ^ ((4 : ℝ) / 3)

Sources

• J. Spencer, E. Szemerédi, W. T. Trotter Jr., Unit distances in the Euclidean plane, in Graph Theory and Combinatorics (Cambridge 1983), Academic Press, 1984. Short crossing-number proof: L. A. Székely, Crossing numbers and hard Erdős problems in discrete geometry, Combin. Probab. Comput. 6 (1997). Best constant: P. Ágoston, D. Pálvölgyi, An improved constant factor for the unit distance problem, Studia Sci. Math. Hungar. 59 (2022). Problem unit_distance_upper_bound of the lean-eval benchmark.

Uses 1

Statement usesNumber of unit-distance pairs in a planar point set

AbbreviationEuclidean plane for Erdős Problem 652#✓fully proved

The real Euclidean plane is the space \(\mathbb{R}^2\) of pairs of real numbers with the Euclidean inner product and norm.

abbrev Plane := EuclideanSpace ℝ (Fin 2)

Used by 2

Used byPoints with few distinct distances · Many points with few distinct distances

DefinitionPoints with few distinct distances#✓fully proved

For a finite set \(X\) of points in the Euclidean plane and a real number \(t\), the number of points \(x \in X\) such that the number of distinct distances from \(x\) to the other points of \(X\) is less than \(t\).

noncomputable def countSmallPoints (X : Finset Plane) (threshold : ℝ) : ℕ := by
  classical
  exact (X.filter (fun x => (distinctDistancesFrom X x : ℝ) < threshold)).card

Uses 2 · Used by 1

Statement usesEuclidean plane for Erdős Problem 652 · Number of distinct distances from a point

Used byMany points with few distinct distances

DefinitionMany points with few distinct distances#✓fully proved

For natural numbers \(n\), \(k\) and a real number \(c\), the property that some set \(X\) of exactly \(n\) points in the Euclidean plane contains at least \(k\) points \(x\) such that the number of distinct distances from \(x\) to the other points of \(X\) is less than \(c\sqrt{n}\).

For \(1 \le k \le n\) this says that, with the points of \(X\) ordered by this number, the \(k\)-th smallest value is less than \(c\sqrt{n}\).

def HasSmallKth (n k : ℕ) (bound : ℝ) : Prop :=
  ∃ X : Finset Plane, X.card = n ∧
    k ≤ countSmallPoints X (bound * Real.sqrt (n : ℝ))

Uses 2 · Used by 1

Statement usesEuclidean plane for Erdős Problem 652 · Points with few distinct distances

Used byAdmissible constants in Erdős Problem 652

DefinitionAdmissible constants in Erdős Problem 652#✓fully proved

A real number \(c\) is admissible for \(k \in \mathbb{N}\) if there is \(N\) such that for every \(n \ge N\) some set \(X\) of exactly \(n\) points in the Euclidean plane contains at least \(k\) points \(x\) such that the number of distinct distances from \(x\) to the other points of \(X\) is less than \(c\sqrt{n}\).

def isAdmissibleBound (k : ℕ) (bound : ℝ) : Prop :=
  ∃ N : ℕ, ∀ n : ℕ, N ≤ n → HasSmallKth n k bound

Uses 1 · Used by 1

Statement usesMany points with few distinct distances

Used byThe Erdős constant \(\alpha_k\)

DefinitionThe Erdős constant \(\alpha_k\)#✓fully proved

For \(k \in \mathbb{N}\), \(\alpha_k\) is the infimum of the set of real numbers that are admissible for \(k\): the reals \(c\) for which there is \(N\) such that for every \(n \ge N\) some set \(X\) of exactly \(n\) points in the Euclidean plane contains at least \(k\) points \(x\) such that the number of distinct distances from \(x\) to the other points of \(X\) is less than \(c\sqrt{n}\). If this set is empty or unbounded below, \(\alpha_k = 0\).

noncomputable def erdosAlpha (k : ℕ) : ℝ :=
  sInf { bound : ℝ | isAdmissibleBound k bound }

Uses 1 · Used by 1

Statement usesAdmissible constants in Erdős Problem 652

Used byErdős Problem 652

DefinitionErdős Problem 652#✓fully proved

For a finite set \(X\) of points in the Euclidean plane and \(x \in X\), let \(R_X(x)\) be the number of distinct distances from \(x\) to the other points of \(X\). For \(k \in \mathbb{N}\) let \(\alpha_k\) be the infimum of the reals \(c\) for which there is \(N\) such that for every \(n \ge N\) some set \(X\) of exactly \(n\) points in the plane has at least \(k\) points \(x\) with \(R_X(x) < c\sqrt{n}\) (an empty set or a set unbounded below is given infimum \(0\)). The proposition is that \(\alpha_k \to \infty\) as \(k \to \infty\).

def conjecture : Prop :=
  Filter.Tendsto erdosAlpha Filter.atTop Filter.atTop

Uses 1 · Used by 1

Statement usesThe Erdős constant \(\alpha_k\)

Used byErdős Problem 652 is true

TheoremErdős Problem 652 is true#●ready to prove

For a finite set \(X\) of points in the Euclidean plane and \(x \in X\), let \(R_X(x)\) be the number of distinct distances from \(x\) to the other points of \(X\). For \(k \in \mathbb{N}\) let \(\alpha_k\) be the infimum of the reals \(c\) for which there is \(N\) such that for every \(n \ge N\) some set \(X\) of exactly \(n\) points in the plane has at least \(k\) points \(x\) with \(R_X(x) < c\sqrt{n}\) (an empty set or a set unbounded below is given infimum \(0\)). Then \(\alpha_k \to \infty\) as \(k \to \infty\).

Mathialagan proved that for \(2 \le m \le n^{1/3}\), some point of an \(m\)-point set determines \(\Omega(\sqrt{mn})\) distances to an \(n\)-point set; with Elekes's circle-grid construction this gives \(\alpha_k = \Theta(\sqrt{k})\).

public theorem_wanted conjecture_holds : conjecture

Sources

• S. Mathialagan, On bipartite distinct distances in the plane, Electronic Journal of Combinatorics 28(4) (2021) P4.33, arXiv:1912.01883, https://arxiv.org/abs/1912.01883.

Uses 1

Statement usesErdős Problem 652

DefinitionRich distances#✓fully proved

For a finite set \(A\) of points in the Euclidean plane and a natural number \(k\), the rich distances of \(A\) at level \(k\) are the distances \(d\) between two distinct points of \(A\) such that at least \(k\) unordered pairs of distinct points of \(A\) are at distance \(d\).

noncomputable def richDistances (A : Finset (EuclideanSpace ℝ (Fin 2)))
    (k : ℕ) : Finset ℝ :=
  (distanceSet A).filter fun d => k ≤ distanceMultiplicity A d

Uses 2 · Used by 2

Statement usesMultiplicity of a distance · Distance set of a finite point set

Used byStatement of Erdős Problem 756 on rich distances · Maximal number of rich distances

DefinitionMaximal number of rich distances#✓fully proved

For a natural number \(n\), this is the largest, over all sets \(A\) of \(n\) points in the Euclidean plane, of the number of rich distances of \(A\) at level \(n + 1\), that is, of distances that occur for at least \(n + 1\) unordered pairs of distinct points of \(A\).

noncomputable def maxRichDistances (n : ℕ) : ℕ :=
  sSup {(richDistances A (n + 1)).card | (A : Finset (EuclideanSpace ℝ (Fin 2))) (_ : A.card = n)}

Uses 1 · Used by 1

Statement usesRich distances

Used byStatement of Erdős Problem 756 on rich distances

DefinitionStatement of Erdős Problem 756 on rich distances#✓fully proved

For a finite set \(A\) of points in the Euclidean plane, call a distance \(k\)-rich for \(A\) if at least \(k\) unordered pairs of distinct points of \(A\) lie at that distance, and let \(f(n)\) be the largest number of \((n+1)\)-rich distances of a set of \(n\) points. This is the assertion that there is a constant \(C\) with \(n \le C f(n)\) for all sufficiently large \(n\); that for every \(n\) there is a set of \(n\) points with at least \(\lfloor n/4 \rfloor\) distances that are \((n+1)\)-rich; and that for every \(m \ge 1\) there is an \(N\) such that for every \(n \ge N\) there is a set of \(n\) points with at least \(\lfloor n/(2(m+1)) \rfloor\) distances that are \((n+m)\)-rich.

def conjecture : Prop :=
  ((fun n : ℕ => (n : ℝ)) =O[atTop] (fun n : ℕ => (maxRichDistances n : ℝ))) ∧
  (∀ n : ℕ, ∃ A : Finset (EuclideanSpace ℝ (Fin 2)),
    A.card = n ∧ n / 4 ≤ (richDistances A (n + 1)).card) ∧
  (∀ m : ℕ, 1 ≤ m → ∀ᶠ n : ℕ in atTop, ∃ A : Finset (EuclideanSpace ℝ (Fin 2)),
    A.card = n ∧ n / (2 * (m + 1)) ≤ (richDistances A (n + m)).card)

Uses 2 · Used by 1

Statement usesMaximal number of rich distances · Rich distances

Used byBhowmick's theorem on rich distances

TheoremBhowmick's theorem on rich distances#●ready to prove

For a finite set \(A\) of points in the Euclidean plane, call a distance \(k\)-rich for \(A\) if at least \(k\) unordered pairs of distinct points of \(A\) lie at that distance, and let \(f(n)\) be the largest number of \((n+1)\)-rich distances of a set of \(n\) points. Then there is a constant \(C\) with \(n \le C f(n)\) for all sufficiently large \(n\); for every \(n\) there is a set of \(n\) points with at least \(\lfloor n/4 \rfloor\) distances that are \((n+1)\)-rich; and for every \(m \ge 1\) there is an \(N\) such that for every \(n \ge N\) there is a set of \(n\) points with at least \(\lfloor n/(2(m+1)) \rfloor\) distances that are \((n+m)\)-rich.

public theorem_wanted conjecture_holds : conjecture

Sources

• K. Bhowmick, A problem of Erdős about rich distances, arXiv:2407.01174 (2024), https://arxiv.org/abs/2407.01174; External Lean proof of Erdős Problem 756, https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/v4.29.1/ErdosProblems/Erdos756.lean.

Uses 1

Statement usesStatement of Erdős Problem 756 on rich distances

22 fully proved7 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.