1. FormalConjectures
  2. ErdosProblems
  3. «96»
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Erdős Problem 96

Reference: erdosproblems.com/96

open Filteropen EuclideanGeometryopen scoped EuclideanGeometry namespace Erdos96open Finset

The set of all possible numbers of unit distances determined by the vertices of a convex $n$-gon.

noncomputable def convexUnitDistanceCounts (n : ℕ) : Set ℕ := {unitDistancePairsCount points | (points : Finset ℝ²) (_ : points.card = n) (_ : ConvexIndep points)}

This lemma confirms that the set of possible unit-distance counts is bounded above, which ensures that taking the supremum (sSup) is a well-defined operation. The trivial upper bound is the total number of pairs of points, $\binom{n}{2}$.

@[category test, AMS 52] theorem convexUnitDistanceCounts_bddAbove (n : ℕ) : BddAbove <| convexUnitDistanceCounts n := n:ℕ⊢ BddAbove (convexUnitDistanceCounts n) n:ℕ⊢ BddAbove {x | ∃ points, ∃ (_ : #points = n) (_ : ConvexIndep ↑points), unitDistancePairsCount points = x} n:ℕ⊢ BddAbove {x | ∃ points, ∃ (_ : #points = n) (_ : ConvexIndep ↑points), #({p ∈ points.offDiag | dist p.1 p.2 = 1}) / 2 = x} n:ℕ⊢ n.choose 2 ∈ upperBounds {x | ∃ points, ∃ (_ : #points = n) (_ : ConvexIndep ↑points), #({p ∈ points.offDiag | dist p.1 p.2 = 1}) / 2 = x} points:Finset ℝ²w✝:ConvexIndep ↑points⊢ #({p ∈ points.offDiag | dist p.1 p.2 = 1}) / 2 ≤ (#points).choose 2 points:Finset ℝ²w✝:ConvexIndep ↑points⊢ #({p ∈ points.offDiag | dist p.1 p.2 = 1}) / 2 ≤ #points * (#points - 1) / 2 have hle : (points.offDiag.filter fun p : ℝ² × ℝ² => dist p.1 p.2 = 1).card ≤ points.offDiag.card := n:ℕ⊢ BddAbove (convexUnitDistanceCounts n) All goals completed! 🐙 points:Finset ℝ²w✝:ConvexIndep ↑pointshle:#({p ∈ points.offDiag | dist p.1 p.2 = 1}) ≤ #points.offDiag := card_filter_le points.offDiag fun p => dist p.1 p.2 = 1hdiv:#({p ∈ points.offDiag | dist p.1 p.2 = 1}) / 2 ≤ #points.offDiag / 2 := Nat.div_le_div_right hle⊢ #({p ∈ points.offDiag | dist p.1 p.2 = 1}) / 2 ≤ #points * (#points - 1) / 2 All goals completed! 🐙

The maximum number of unit distances determined by the vertices of a convex $n$-gon. This function is often denoted as $U_c(n)$ in combinatorics.

noncomputable def maxConvexUnitDistances (n : ℕ) : ℕ := sSup (convexUnitDistanceCounts n)

If $n$ points in $\mathbb{R}^2$ form a convex polygon then there are $O(n)$ many pairs which are distance $1$ apart.

@[category research open, AMS 52] theorem declaration uses 'sorry'erdos_96 : answer(sorry) ↔ (fun n => (maxConvexUnitDistances n : ℝ)) =O[atTop] fun n => (n : ℝ) := ⊢ True ↔ (fun n => ↑(maxConvexUnitDistances n)) =O[atTop] fun n => ↑n All goals completed! 🐙 end Erdos96