/-
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 FormalConjecturesUtilErdős Problem 91
Reference:
[Er87b] Erdős, P., Some combinatorial and metric problems in geometry. Intuitive geometry (Siófok, 1985) (1987), 167-177.
[Ko24c] Z. Kovács, A note on Erdős's mysterious remark. arXiv:2412.05190 (2024).
open Finset EuclideanGeometry Filternamespace Erdos91A set $A$ is 'optimal' if it has $n$ points and achieves the minimum distance count.
noncomputable def IsOptimal (A : Finset ℝ²) (n : ℕ) : Prop :=
A.card = n ∧ distinctDistances A = minimalDistinctDistances nTwo finite sets of points in $\mathbb{R}^2$ are similar if one can be mapped to the other by a DilationEquiv.
def DilationEquivSimilar (A B : Finset ℝ²) : Prop :=
∃ f : ℝ² ≃ᵈ ℝ², (f '' A) = BEquilateral triangle with unit side length, resting on the x-axis with one vertex at the origin.
noncomputable def equiTriangle : Finset ℝ² := {!2[0, 0], !2[1, 0], !2[1 / 2, Real.sqrt 3 / 2]}noncomputable def unitSquare : Finset ℝ² := {!2[0, 0], !2[0, 1], !2[1, 0], !2[1, 1]}Regular 7-gon with unit side length, touching both axes in the first quadrant.
noncomputable def circleSeven : Finset ℝ² :=
let r := 1 / (2 * Real.sin (Real.pi / 7))
let cx := r * Real.cos (Real.pi / 7)
let cy := r * Real.sin (4 * Real.pi / 7)
(Finset.range 7).image fun k : ℕ =>
!2[r * Real.cos (2 * Real.pi * ↑k / 7) + cx, r * Real.sin (2 * Real.pi * ↑k / 7) + cy]Wheel graph on 7 vertices (center + regular hexagon) with unit side length, touching both axes in the first quadrant.
noncomputable def wheelSeven : Finset ℝ² :=
{!2[1, Real.sqrt 3 / 2],
!2[2, Real.sqrt 3 / 2],
!2[3 / 2, Real.sqrt 3],
!2[1 / 2, Real.sqrt 3],
!2[0, Real.sqrt 3 / 2],
!2[1 / 2, 0],
!2[3 / 2, 0]}All goals completed! 🐙⟩@[category test, AMS 52]
lemma erdos_91.test.equiTriangle_unique_optimal :
∀ A : Finset ℝ², IsOptimal A 3 → DilationEquivSimilar A equiTriangle := ⊢ ∀ (A : Finset ℝ²), IsOptimal A 3 → DilationEquivSimilar A equiTriangle
All goals completed! 🐙@[category test, AMS 52]
lemma erdos_91.test.unitSquare_optimal : IsOptimal unitSquare 4 := ⊢ IsOptimal unitSquare 4
All goals completed! 🐙@[category test, AMS 52]
lemma erdos_91.test.circleSeven_optimal : IsOptimal circleSeven 7 := ⊢ IsOptimal circleSeven 7
All goals completed! 🐙@[category test, AMS 52]
lemma erdos_91.test.wheelSeven_optimal : IsOptimal wheelSeven 7 := ⊢ IsOptimal wheelSeven 7
All goals completed! 🐙@[category test, AMS 52]
lemma erdos_91.test.dissimilar_circleSeven_wheelSeven :
¬DilationEquivSimilar circleSeven wheelSeven := ⊢ ¬DilationEquivSimilar circleSeven wheelSeven
All goals completed! 🐙The predicate on $n$ asserting all $A, B\subset \mathbb{R}^2$, with $\lvert A\rvert=n = \lvert B\rvert$, which minimise the number of distinct points for all sets with $n$ elements are similar.
def UniqueMinimizer (n : ℕ) : Prop :=
∀ A B : Finset ℝ², IsOptimal A n → IsOptimal B n → DilationEquivSimilar A BSuppose $A\subset \mathbb{R}^2$ has $\lvert A\rvert=n$ and minimises the number of distinct distances between points in $A$. Prove that for large $n$ there are at least two (and probably many) such $A$ which are non-similar.
@[category research open, AMS 52]
theorem erdos_91 :
(∀ᶠ n : ℕ in atTop, ¬ UniqueMinimizer n) ↔ answer(sorry) := ⊢ (∀ᶠ (n : ℕ) in atTop, ¬UniqueMinimizer n) ↔ True
All goals completed! 🐙For $n = 3$ the equilateral triangle is the only such set.
@[category research solved, AMS 52]
theorem erdos_91.variants.three : UniqueMinimizer 3 := ⊢ UniqueMinimizer 3
All goals completed! 🐙For $n=4$ the square or two equilateral triangles sharing an edge give two non-similar examples.
@[category research solved, AMS 52]
theorem erdos_91.variants.four : ¬ UniqueMinimizer 4 := ⊢ ¬UniqueMinimizer 4
All goals completed! 🐙For $n = 5$ the regular pentagon is the unique such set (which has two distinct distances). Erdős mysteriously remarks in [Er90] this was proved by 'a colleague'. (In [Er87b] this is described as 'a colleague from Zagreb (unfortunately I do not have his letter)'.) A published proof of this fact is provided by Kovács [Ko24c].
@[category research solved, AMS 52]
theorem erdos_91.variants.five : UniqueMinimizer 5 := ⊢ UniqueMinimizer 5
All goals completed! 🐙In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for $n = 6$.
@[category research solved, AMS 52]
theorem erdos_91.variants.six: ¬ UniqueMinimizer 6 := ⊢ ¬UniqueMinimizer 6
All goals completed! 🐙In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for $n = 7$.
@[category research solved, AMS 52]
theorem erdos_91.variants.seven: ¬ UniqueMinimizer 7 := ⊢ ¬UniqueMinimizer 7
All goals completed! 🐙In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for $n = 8$.
@[category research solved, AMS 52]
theorem erdos_91.variants.eight: ¬ UniqueMinimizer 8 := ⊢ ¬UniqueMinimizer 8
All goals completed! 🐙In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for $n = 9$.
@[category research solved, AMS 52]
theorem erdos_91.variants.nine: ¬ UniqueMinimizer 9 := ⊢ ¬UniqueMinimizer 9
All goals completed! 🐙end Erdos91