97.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

12 declarations, 5 contain sorry, 0 declared as axioms

Erdős Problem 97

Reference: erdosproblems.com/97

Imports (1)

FormalConjecturesUtil

def Erdos97.HasNEquidistantPointsAt A set of points $A$ has n equidistant points at $p$ if there exist at least $n$ other points in $A$ that are equidistant from $p$ line 37 source
Source documentation
A set of points $A$ has n equidistant points at $p$ if there exist at least $n$ other points in $A$ that are equidistant from $p$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat
Proof uses: Exists, And, GT.gt, GE.ge, Finset.card, Finset.filter, Eq, Dist.dist, ENNReal
16 instances, coercions and auxiliary constants left out.
```
def HasNEquidistantPointsAt (n : ℕ) (A : Finset ℝ²) (p : ℝ²) : Prop :=
…
```
def Erdos97.HasNEquidistantPointsOn A set of points $A$ has n equidistant points on a set of points $B$ if for every point in $B$, there exist at least $n$ other points in $A$ that are equidistant from it line 44 source
Source documentation
A set of points $A$ has n equidistant points on a set of points $B$ if for every point in $B$, there exist at least $n$ other points in $A$ that are equidistant from it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat
Proof uses: Membership.mem, Erdos97.HasNEquidistantPointsAt
4 instances, coercions and auxiliary constants left out.
```
def HasNEquidistantPointsOn (n : ℕ) (A : Finset ℝ²) (B : Finset ℝ²) : Prop :=
…
```
def Erdos97.HasNEquidistantProperty A set of points $A$ has n equidistant property if for every point in $A$, there exist at least $n$ other points in $A$ that are equidistant from it line 51 source
Source documentation
A set of points $A$ has n equidistant property if for every point in $A$, there exist at least $n$ other points in $A$ that are equidistant from it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat
Proof uses: Erdos97.HasNEquidistantPointsOn
2 instances, coercions and auxiliary constants left out.
```
def HasNEquidistantProperty (n : ℕ) (A : Finset ℝ²) : Prop :=
…
```
def Erdos97.HasNUnitDistancePointsAt A set of points $A$ has n unit distance points at $p$ if there exist at least $n$ other points in $A$ that are at unit distance from $p$ line 58 source
Source documentation
A set of points $A$ has n unit distance points at $p$ if there exist at least $n$ other points in $A$ that are at unit distance from $p$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat
Proof uses: GE.ge, Finset.card, Finset.filter, Eq, Dist.dist, ENNReal
15 instances, coercions and auxiliary constants left out.
```
def HasNUnitDistancePointsAt (n : ℕ) (A : Finset ℝ²) (p : ℝ²) : Prop :=
…
```
def Erdos97.HasNUnitDistancePointsOn A set of points $A$ has n unit distance points on a set of points $B$ if for every point in $B$, there exist at least $n$ other points in $A$ that are at unit distance from it line 65 source
Source documentation
A set of points $A$ has n unit distance points on a set of points $B$ if for every point in $B$, there exist at least $n$ other points in $A$ that are at unit distance from it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat
Proof uses: Membership.mem, Erdos97.HasNUnitDistancePointsAt
4 instances, coercions and auxiliary constants left out.
```
def HasNUnitDistancePointsOn (n : ℕ) (A : Finset ℝ²) (B : Finset ℝ²) : Prop :=
…
```
def Erdos97.HasNUnitDistanceProperty A set of points $A$ has n unit distance property if for every point in $A$, there exist at least $n$ other points in $A$ that are at unit distance from it line 72 source
Source documentation
A set of points $A$ has n unit distance property if for every point in $A$, there exist at least $n$ other points in $A$ that are at unit distance from it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat
Proof uses: Erdos97.HasNUnitDistancePointsOn
2 instances, coercions and auxiliary constants left out.
```
def HasNUnitDistanceProperty (n : ℕ) (A : Finset ℝ²) : Prop :=
…
```
theorem Erdos97.erdos_97 Does every convex polygon have a vertex with no other 4 vertices equidistant from it? sorry line 79 source
Source documentation
Does every convex polygon have a vertex with no other 4 vertices equidistant from it?

depends on sorry what this means
Statement uses: Iff, True, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Finset.Nonempty, EuclideanGeometry.ConvexIndep, Not, Erdos97.HasNEquidistantProperty
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_97 :
    answer(sorry) ↔ ∀ A : Finset ℝ², A.Nonempty → ConvexIndep A → ¬HasNEquidistantProperty 4 A := by
…
```
Mentions: Erdos97.HasNEquidistantProperty
theorem Erdos97.erdos_97.variants.three_equidistant Documented declaration: three_equidistant sorry line 93 source
Source documentation
Erdős originally conjectured this (in [Er46b]) with no 3 vertices equidistant, but Danzer found a convex polygon on 9 points such that every vertex has three vertices equidistant from it (but this distance depends on the vertex). Danzer's construction is explained in [Er87b].
[Er46b] Erdős, P., On sets of distances of $n$ points. Amer. Math. Monthly (1946), 248-250. [Er87b] Erdős, P., Some combinatorial and metric problems in geometry. Intuitive geometry (Siófok, 1985), 167-177.

depends on sorry what this means
Statement uses: Exists, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, And, Finset.Nonempty, EuclideanGeometry.ConvexIndep, Erdos97.HasNEquidistantProperty
Proof uses: WithLp.toLp, ENNReal, Matrix.vecCons, Neg.neg, Real.sqrt, Matrix.vecEmpty, HMul.hMul, HDiv.hDiv, Exists.intro, Insert.insert, Singleton.singleton, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_97.variants.three_equidistant :
    ∃ A : Finset ℝ², A.Nonempty ∧ ConvexIndep A ∧ HasNEquidistantProperty 3 A := by
…
```
Mentions: Erdos97.HasNEquidistantProperty
theorem Erdos97.erdos_97.variants.k_equidistant Erdős also conjectured that there is a $k$ for which every convex polygon has a vertex with no other $k$ vertices equidistant from it sorry line 112 source
Source documentation
Erdős also conjectured that there is a $k$ for which every convex polygon has a vertex with no other $k$ vertices equidistant from it.

depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Finset.Nonempty, EuclideanGeometry.ConvexIndep, Not, Erdos97.HasNEquidistantProperty
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_97.variants.k_equidistant : answer(sorry) ↔
    ∃ k : ℕ, ∀ A : Finset ℝ², A.Nonempty → ConvexIndep A → ¬HasNEquidistantProperty k A := by
…
```
Mentions: Erdos97.HasNEquidistantProperty
theorem Erdos97.erdos_97.variants.three_unit_distance Fishburn and Reeds [FiRe92] have found a convex polygon on 20 points such that every vertex has three vertices equidistant from it (and this distance is the same for all vertices) sorry line 123 source
Source documentation
Fishburn and Reeds [FiRe92] have found a convex polygon on 20 points such that every vertex has three vertices equidistant from it (and this distance is the same for all vertices).
[FiRe92] Fishburn, P. C. and Reeds, J. A., Unit distances between vertices of a convex polygon. Comput. Geom. (1992), 81-91.

depends on sorry what this means
Statement uses: Exists, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, And, Finset.Nonempty, EuclideanGeometry.ConvexIndep, Erdos97.HasNUnitDistanceProperty
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_97.variants.three_unit_distance :
    ∃ A : Finset ℝ², A.Nonempty ∧ ConvexIndep A ∧ HasNUnitDistanceProperty 3 A := by
…
```
Mentions: Erdos97.HasNUnitDistanceProperty
def Erdos97.IsCut A two-part partition $\{A, B\}$ of $V$ is a cut if the convex hulls of $A$ and $B$ are disjoint line 130 source
Source documentation
A two-part partition $\{A, B\}$ of $V$ is a cut if the convex hulls of $A$ and $B$ are disjoint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat
Proof uses: And, Eq, Union.union, ENNReal, Disjoint, Set, ClosureOperator, convexHull
39 instances, coercions and auxiliary constants left out.
```
def IsCut (V A B : Finset ℝ²) : Prop :=
…
```
theorem Erdos97.erdos_97.variants.three_unit_distance_cut_min Fishburn and Reeds [FiRe92] also proved that the smallest sorry line 140 source
Source documentation
Fishburn and Reeds [FiRe92] also proved that the smallest $n$ for which there exists a convex $n$-gon and a cut $\{A, B\}$ of its vertices such that $|\{b \in B : d(a, b) = 1\}| ≥ 3$ for all $a \in A$, and $|\{a \in A : d(a, b) = 1\}| ≥ 3$ for all $b \in B$, is $n = 20$.

depends on sorry what this means
Statement uses: Eq, Nat, InfSet.sInf, Set.ofPred, Exists, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, And, Finset.card, EuclideanGeometry.ConvexIndep, Finset.Nonempty, Erdos97.IsCut, Erdos97.HasNUnitDistancePointsOn
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_97.variants.three_unit_distance_cut_min :
    sInf {n : ℕ | ∃ (V : Finset ℝ²) (A B : Finset ℝ²),
      n = V.card ∧ ConvexIndep V ∧ A.Nonempty ∧ B.Nonempty ∧ IsCut V A B ∧
      HasNUnitDistancePointsOn 3 B A ∧ HasNUnitDistancePointsOn 3 A B} = 20 := by
…
```
Mentions: Erdos97.IsCut, Erdos97.HasNUnitDistancePointsOn