Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated


Claim. Let f(d)f(d) be the largest size of an isosceles set in Rd\mathbb{R}^d, g(d)g(d) the largest size of a Euclidean two-distance set in Rd\mathbb{R}^d, s(d)s(d) the largest size of a spherical two-distance set in Rd\mathbb{R}^d, and h(d)h(d) the largest size of an isosceles set in Rd\mathbb{R}^d that is not a two-distance set. Przemek Chojecki's note The Euclidean isosceles-set problem and Erdős Problem 503, posted to the site's discussion thread on 2026-04-22, states as Theorem 1.1 that for every d≥2d\ge2

h(d)≤max⁡{s(d)+1, s(d−1)+3}and hencef(d)=max⁡{g(d), s(d)+1, s(d−1)+3},h(d)\le\max\{s(d)+1,\ s(d-1)+3\} \quad\text{and hence}\quad f(d)=\max\{g(d),\ s(d)+1,\ s(d-1)+3\},

and that f(1)=3f(1)=3. The lower bound comes from two constructions: a spherical two-distance set with the center of its sphere, and a spherical two-distance set in a hyperplane with the center and two symmetric points on the perpendicular through it. The upper bound applies the complete decomposition theorem for isosceles sets with more than two distances, Theorem 2.15 of Ionin's paper, which credits it to Blokhuis; the theorem splits such a set into two-distance blocks, with the Delsarte–Goethals–Seidel bound for spherical two-distance sets and Blokhuis's bound for Euclidean ones. Chojecki writes in the thread that the claimant obtained the note with GPT-5.4 Pro and the accompanying Lean file with Aristotle. The note's Corollary 6.4 derives, from Musin's value s(22)=275s(22)=275 and Blokhuis's bound (242)=276\binom{24}{2}=276, that

f(22)=276,f(22)=276,

and, from Barg and Yu's value s(23)=276s(23)=276, that h(23)=278h(23)=278 and f(23)=max⁡{g(23),278}f(23)=\max\{g(23),278\}, so f(23)≥278f(23)\ge278; this derivation uses only the two constructions and Blokhuis's bound, not the reduction. Corollary 6.3 recovers the values for d≤8d\le8 from the identity and the known two-distance maxima; they agree with the table on Ionin's claim page.

Revision. A gap was raised in the thread on 2026-05-26 by Koizumi: the note's case analysis assumed that every non-last block of the decomposition has at least three points, while Ionin's definition allows a block of two. The revised note Euclidean isosceles sets and two-distance extremal functions, the second preprint link, posted on 2026-05-27, handles the two-point block case by a polynomial lemma on two concentric shells (Section 5) and a separate case analysis (Section 6), keeps Theorem 1.1 unchanged and drops the corollaries. Chojecki writes that they produced the repair with GPT-5.5 Pro. The value f(22)=276f(22)=276 is unaffected by the gap, since its derivation does not use the reduction; a thread post of 2026-05-29 repeats it.

Covers. The instance d=22d=22 of Problem 503, answered 276276, which meets Blokhuis's bound; the lower bound f(23)≥278f(23)\ge278; and the identity f(d)=max⁡{g(d),s(d)+1,s(d−1)+3}f(d)=\max\{g(d),s(d)+1,s(d-1)+3\} for every d≥2d\ge2, which reduces the problem to the two-distance extremal functions but determines no further dimension by itself, since g(d)g(d) and s(d)s(d) are known only in some dimensions.

Depends on. Ionin's claim page, whose paper states, as its Theorem 2.15 credited to Blokhuis, the complete decomposition theorem the reduction rests on. The two-distance bounds and values (Delsarte, Goethals and Seidel 1977; Blokhuis 1984; Musin 2009; Barg and Yu 2013) are literature the note cites.

Acceptance. Neither note is refereed, and no reviewed evidence is listed: the site labels the problem OPEN and does not cite the notes, and a thread user's statement of 2026-05-28 that the revised note looks correct is not acceptance. The Lean file, the formalization link, states the decomposition theorem of Ionin's Theorem 2.15, the two-distance bounds, the two lower constructions and the values s(22)=275s(22)=275 and s(23)=276s(23)=276 as hypotheses of its theorems and proves the case analysis and the corollaries from them; it leaves the cited results unproved, has not been built or audited in this repository, and gives no formalized evidence.