91.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

21 declarations, 13 contain sorry, 0 declared as axioms

Erdő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).
erdosproblems.com/91

Imports (1)

FormalConjecturesUtil

def Erdos91.IsOptimal A set $A$ is 'optimal' if it has $n$ points and achieves the minimum distance count line 37 source
Source documentation
A set $A$ is 'optimal' if it has $n$ points and achieves the minimum distance count.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: And, Eq, Finset.card, distinctDistances, ENNReal, minimalDistinctDistances
11 instances, coercions and auxiliary constants left out.
```
noncomputable def IsOptimal (A : Finset ℝ²) (n : ℕ) : Prop :=
…
```
def Erdos91.DilationEquivSimilar Two finite sets of points in $\mathbb{R}^2$ are similar if one can be mapped to the other by a DilationEquiv line 42 source
Source documentation
Two finite sets of points in $\mathbb{R}^2$ are similar if one can be mapped to the other by a DilationEquiv.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: Exists, DilationEquiv, ENNReal, Eq, Set, Set.image
18 instances, coercions and auxiliary constants left out.
```
def DilationEquivSimilar (A B : Finset ℝ²) : Prop :=
…
```
def Erdos91.equiTriangle Equilateral triangle with unit side length, resting on the x-axis with one vertex at the origin line 46 source
Source documentation
Equilateral triangle with unit side length, resting on the x-axis with one vertex at the origin.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: Insert.insert, WithLp, ENNReal, WithLp.toLp, Matrix.vecCons, Matrix.vecEmpty, Singleton.singleton, HDiv.hDiv, Real.sqrt
23 instances, coercions and auxiliary constants left out.
```
noncomputable def equiTriangle : Finset ℝ² := {!₂[0, 0], !₂[1, 0], !₂[1 / 2, Real.sqrt 3 / 2]}
```
def Erdos91.unitSquare line 48 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: Insert.insert, WithLp, ENNReal, WithLp.toLp, Matrix.vecCons, Matrix.vecEmpty, Singleton.singleton
18 instances, coercions and auxiliary constants left out.
def Erdos91.circleSeven Regular 7-gon with unit side length, touching both axes in the first quadrant line 51 source
Source documentation
Regular 7-gon with unit side length, touching both axes in the first quadrant.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: HDiv.hDiv, HMul.hMul, Real.sin, Real.pi, Real.cos, Finset.image, ENNReal, WithLp.toLp, Matrix.vecCons, HAdd.hAdd, Matrix.vecEmpty, Finset.range
25 instances, coercions and auxiliary constants left out.
```
noncomputable def circleSeven : Finset ℝ² :=
…
```
def Erdos91.wheelSeven Wheel graph on 7 vertices (center + regular hexagon) with unit side length, touching both axes in the first quadrant line 60 source
Source documentation
Wheel graph on 7 vertices (center + regular hexagon) with unit side length, touching both axes in the first quadrant.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: Insert.insert, WithLp, ENNReal, WithLp.toLp, Matrix.vecCons, HDiv.hDiv, Real.sqrt, Matrix.vecEmpty, Singleton.singleton
23 instances, coercions and auxiliary constants left out.
```
noncomputable def wheelSeven : Finset ℝ² :=
…
```
lemma Erdos91.erdos_91.test.equiTriangle_optimal line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Erdos91.IsOptimal, Erdos91.equiTriangle, OfNat.ofNat, Nat
Proof uses: Eq, Finset.card, EuclideanSpace, Real, Fin, of_eq_true, Eq.trans, True, congrFun', congrArg, HAdd.hAdd, Insert.insert, WithLp, ENNReal, Finset, WithLp.toLp, Matrix.vecCons, Matrix.vecEmpty, Singleton.singleton, Inv.inv and 191 more
200 instances, coercions and auxiliary constants left out.

Tactic trace: 58 steps
Open to load the checked before-and-after goal states.
lemma Erdos91.erdos_91.test.equiTriangle_unique_optimal sorry line 115 source
depends on sorry what this means
Statement uses: Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Erdos91.IsOptimal, Erdos91.DilationEquivSimilar, Erdos91.equiTriangle
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Erdos91.erdos_91.test.unitSquare_optimal sorry line 120 source
depends on sorry what this means
Statement uses: Erdos91.IsOptimal, Erdos91.unitSquare, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Erdos91.erdos_91.test.circleSeven_optimal sorry line 124 source
depends on sorry what this means
Statement uses: Erdos91.IsOptimal, Erdos91.circleSeven, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Erdos91.erdos_91.test.wheelSeven_optimal sorry line 128 source
depends on sorry what this means
Statement uses: Erdos91.IsOptimal, Erdos91.wheelSeven, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Erdos91.erdos_91.test.dissimilar_circleSeven_wheelSeven sorry line 132 source
depends on sorry what this means
Statement uses: Not, Erdos91.DilationEquivSimilar, Erdos91.circleSeven, Erdos91.wheelSeven
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Erdos91.UniqueMinimizer Documented declaration: UniqueMinimizer line 141 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Erdos91.IsOptimal, Erdos91.DilationEquivSimilar
1 instances, coercions and auxiliary constants left out.
```
def UniqueMinimizer (n : ℕ) : Prop :=
…
```
theorem Erdos91.erdos_91 Suppose $A\subset \mathbb{R}^2$ has $\lvert A\rvert=n$ and minimises the number of distinct distances between points in $A$ sorry line 150 source
Source documentation
Suppose $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.

depends on sorry what this means
Statement uses: Iff, True, Filter.Eventually, Nat, Not, Erdos91.UniqueMinimizer, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_91 :
    answer(sorry) ↔ ∀ᶠ n : ℕ in atTop, ¬ UniqueMinimizer n := by
…
```
Mentions: Erdos91.UniqueMinimizer
theorem Erdos91.erdos_91.variants.three For $n = 3$ the equilateral triangle is the only such set sorry line 159 source
Source documentation
For $n = 3$ the equilateral triangle is the only such set.

depends on sorry what this means
Statement uses: Erdos91.UniqueMinimizer, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_91.variants.three : UniqueMinimizer 3 := by
…
```
Mentions: Erdos91.UniqueMinimizer
theorem Erdos91.erdos_91.variants.four For $n=4$ the square or two equilateral triangles sharing an edge give two non-similar examples sorry line 168 source
Source documentation
For $n=4$ the square or two equilateral triangles sharing an edge give two non-similar examples.

depends on sorry what this means
Statement uses: Not, Erdos91.UniqueMinimizer, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_91.variants.four : ¬ UniqueMinimizer 4 := by
…
```
Mentions: Erdos91.UniqueMinimizer
theorem Erdos91.erdos_91.variants.five For $n = 5$ the regular pentagon is the unique such set (which has two distinct distances) sorry line 179 source
Source documentation
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].

depends on sorry what this means
Statement uses: Erdos91.UniqueMinimizer, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_91.variants.five : UniqueMinimizer 5 := by
…
```
Mentions: Erdos91.UniqueMinimizer
theorem Erdos91.erdos_91.variants.six In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for $n = 6$ sorry line 186 source
Source documentation
In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for $n = 6$.

depends on sorry what this means
Statement uses: Not, Erdos91.UniqueMinimizer, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_91.variants.six: ¬ UniqueMinimizer 6 := by
…
```
Mentions: Erdos91.UniqueMinimizer
theorem Erdos91.erdos_91.variants.seven In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for $n = 7$ sorry line 194 source
Source documentation
In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for $n = 7$.

depends on sorry what this means
Statement uses: Not, Erdos91.UniqueMinimizer, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_91.variants.seven: ¬ UniqueMinimizer 7 := by
…
```
Mentions: Erdos91.UniqueMinimizer
theorem Erdos91.erdos_91.variants.eight In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for $n = 8$ sorry line 202 source
Source documentation
In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for $n = 8$.

depends on sorry what this means
Statement uses: Not, Erdos91.UniqueMinimizer, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_91.variants.eight: ¬ UniqueMinimizer 8 := by
…
```
Mentions: Erdos91.UniqueMinimizer
theorem Erdos91.erdos_91.variants.nine In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for $n = 9$ sorry line 210 source
Source documentation
In [Er87b] on p.171 Erdős says that there are at least two non-similar examples for $n = 9$.

depends on sorry what this means
Statement uses: Not, Erdos91.UniqueMinimizer, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_91.variants.nine: ¬ UniqueMinimizer 9 := by
…
```
Mentions: Erdos91.UniqueMinimizer