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

5 declarations, 5 contain sorry, 0 declared as axioms

Erdős Problem 503

Reference: erdosproblems.com/503

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100SolvedSet1.lean

theorem Erdos503.erdos_503 What is the size of the largest $A \subseteq \mathbb{R}^n$ such that every three points from $A$ determine an isosceles triangle? sorry line 38 source
Source documentation
What is the size of the largest $A \subseteq \mathbb{R}^n$ such that every three points from $A$ determine an isosceles triangle? That is, for any three points $x$, $y$, $z$ from $A$, at least two of the distances $|x - y|$, $|y - z|$, $|x - z|$ are equal.

depends on sorry what this means
Statement uses: Nat, IsGreatest, Set.ofPred, Exists, Set, EuclideanSpace, Real, Fin, Set.IsIsosceles, OfNat.ofNat, ENNReal, Eq, Set.ncard, sorryAx, Bool.false
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_503 (n : ℕ) :
    IsGreatest {(A.ncard) | (A : Set (ℝ^n)) (hA : A.IsIsosceles)} answer(sorry) := by
…
```
theorem Erdos503.erdos_503.variants.R2 When $n = 2$, the answer is 6 (due to Kelly [ErKe47] - an alternative proof is given by Kovács [Ko24c]) sorry line 49 source
Source documentation
When $n = 2$, the answer is 6 (due to Kelly [ErKe47] - an alternative proof is given by Kovács [Ko24c]).
[ErKe47] Erdős, Paul and Kelly, L. M., Elementary Problems and Solutions: Solutions: E735. Amer. Math. Monthly (1947), 227-229. [Ko24c] Z. Kovács, A note on Erdős's mysterious remark. arXiv:2412.05190 (2024).

depends on sorry what this means
Statement uses: IsGreatest, Nat, Set.ofPred, Exists, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Set.IsIsosceles, ENNReal, Eq, Set.ncard
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_503.variants.R2 :
    IsGreatest {(A.ncard) | (A : Set ℝ²) (hA : A.IsIsosceles)} 6 := by
…
```
theorem Erdos503.erdos_503.variants.R3 When $n = 3$, the answer is 8 (due to Croft [Cr62]) sorry line 59 source
Source documentation
When $n = 3$, the answer is 8 (due to Croft [Cr62]).
[Cr62] Croft, H. T., $9$-point and $7$-point configurations in $3$-space. Proc. London Math. Soc. (3) (1962), 400-424.

depends on sorry what this means
Statement uses: IsGreatest, Nat, Set.ofPred, Exists, Set, EuclideanSpace, Real, Fin, OfNat.ofNat, Set.IsIsosceles, ENNReal, Eq, Set.ncard
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_503.variants.R3 :
    IsGreatest {(A.ncard) | (A : Set ℝ³) (hA : A.IsIsosceles)} 8 := by
…
```
theorem Erdos503.erdos_503.variants.upper_bound The best upper bound known in general is due to Blokhius [Bl84] who showed that $$ |A| \leq \binom{n + 2}{2} $$ [Bl84] Blokhuis, A., Few-distance sets sorry line 72 source
Source documentation
The best upper bound known in general is due to Blokhius [Bl84] who showed that $$ |A| \leq \binom{n + 2}{2} $$
[Bl84] Blokhuis, A., Few-distance sets. (1984), iv+70.

depends on sorry what this means
Statement uses: Nat, Membership.mem, Set, Set.ofPred, Exists, EuclideanSpace, Real, Fin, Set.IsIsosceles, OfNat.ofNat, ENNReal, Eq, Set.ncard, LE.le, Nat.choose, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_503.variants.upper_bound (n : ℕ) :
    ∀ m ∈ {(A.ncard) | (A : Set (ℝ^n)) (hA : A.IsIsosceles)}, m ≤ (n + 2).choose 2 := by
…
```
theorem Erdos503.erdos_503.variants.lower_bound Documented declaration: lower_bound sorry line 83 source
Source documentation
Alweiss has observed a lower bound of $\binom{n + 1}{2}$ follows from considering the subset of $\mathbb{R}^{n + 1}$ formed of all vectors $e_i + e_j$ where $e_i$, $e_j$ are distinct coordinate vectors. This set can be viewed as a subset of some $\mathbb{R}^n$, and is easily checked to have the required property.

depends on sorry what this means
Statement uses: Nat, LE.le, Nat.choose, HAdd.hAdd, OfNat.ofNat, SupSet.sSup, Set.ofPred, Exists, Set, EuclideanSpace, Real, Fin, Set.IsIsosceles, ENNReal, Eq, Set.ncard
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_503.variants.lower_bound (n : ℕ) :
    (n + 1).choose 2 ≤ sSup {(A.ncard) | (A : Set (ℝ^n)) (hA : A.IsIsosceles)} := by
…
```