---

Claim. The first question of Problem 132 holds for $n=8$: every set of eight points in the plane determines two distinct distances each of which occurs between at most eight pairs. Evan Beller's manuscript, posted in the GitHub repository EvanBeller/erdos-132 as paper/erdos132_n8.pdf, argues by contradiction. Counting the $28$ pairs against the lower bound of four distinct distances for eight planar points forces a hypothetical counterexample to have distance multiplicities $(9,9,9,1)$, so its diameter is attained by exactly one pair. Deleting either endpoint of that pair leaves seven points with three distances, which the classification of seven-point three-distance sets makes a regular heptagon or a regular hexagon with its center. The two seven-point sets share six points, and a rigidity lemma for that six-point overlap, proved in the manuscript, forces the two sets to coincide, which contradicts the two distinct diameter endpoints. The argument is a finite case analysis and gives nothing for other values of $n$.

Submission note. Posted to erdosproblems.com as a proof claim by Evan Beller (account b4ller) on 23 August 2026, giving "OpenAI Codex; ChatGPT" as the AI used:

We prove the first assertion of Erdős Problem #132 for n=8. A hypothetical counterexample is forced by pair counting to have distance multiplicities (9,9,9,1), with a unique diametral pair. Deleting either endpoint leaves a seven-point three-distance set, hence a regular heptagon or a regular hexagon with its center by the known classification. The two deletions share six points; a six-point overlap-rigidity lemma forces them to be equal, contradicting the distinct diameter endpoints. Thus every eight-point planar set has two distinct distances occurring at most eight times. Notes: This claim concerns the n=8 case of the first assertion only; the general problem remains open. The proof uses three explicit published results: the Hopf–Pannwitz diameter bound, the known lower bound of four distances for eight planar points, and the classification of seven-point three-distance sets. The complete deduction is formally verified in Lean 4.32.1 conditional on those three literature inputs, with no project-added mathematical axioms, sorry/admit placeholders, unsafe declarations, or native_decide dependencies. An independent exact exhaustive computation also checks the finite overlap analysis. AI assistance is disclosed in the attached writeup. The (9,9,9,1) profile reduction was already present in Zeraoulia's January 2026 working draft, and Chojecki previously made a public unrefereed n=8 proof claim by a different route. No priority claim is made here.

Covers. The first question for $n=8$ only. The question for general $n\ge5$ and the second, asymptotic question are not touched. The site's remarks record the cases $n=5$ and $n=6$ as proved by Erdős and Fishburn [ErFi95].

Depends on. No page of this wiki.

Literature inputs. The deduction takes three published results as inputs, stated as explicit hypotheses and not reproved: the Hopf–Pannwitz bound that the diameter occurs at most $n$ times [HoPa34], the lower bound of four distinct distances among eight planar points, and the classification of seven-point three-distance sets, up to similarity, as the regular heptagon or the regular hexagon with its center. Shinohara's classification of planar three-distance sets (shinohara_2004_classification_three_distance_sets_two_dimensional_euclidean_space) and Erdős and Fishburn's 1996 paper (erdos_fishburn_1996_maximum_planar_sets_that_determine_k_distances), which Marchetto's note cites as the primary source of the seven-point case, are carded in the library.

Claimant and postings. The claim was posted on the site's proof-claims tab on 23 August 2026 from the account b4ller and is credited there to Evan Beller, with the AI systems named on the tab as OpenAI Codex and ChatGPT; the repository's README says that publication, outside review and the proof-claim submission are human actions. The manuscript and the Lean project are linked above at the repository's revision of 30 August 2026. The README reports a Lean 4.32.1 project at a fixed Mathlib revision whose final theorem, erdos132_at_eight, takes the three literature inputs as a hypothesis structure and whose axiom closure is propext, Classical.choice and Quot.sound, together with an exact exhaustive computation that cross-checks the finite overlap analysis outside Lean. None of this was built, run or audited by this corpus, so the page lists no formalized evidence. The claimant's own notes state that the $(9,9,9,1)$ profile reduction already appears in a working draft of Zeraoulia of January 2026, recorded with its note on Zeraoulia's claim page, and that Chojecki had made an earlier public, unrefereed claim of the $n=8$ case by a different route, a thread post of 28 January 2026 without a manuscript, and make no priority claim. The case $n=8$ had already been claimed, by the same deletion of a diametral endpoint and descent to the regular heptagon, closed by an exact search, with a second proof through the eight-point four-distance classification, in Marchetto's note of 5 July 2026 (claim page), and again independently in ienjoymath's note of 25 July 2026 (claim page); the claimant's notes, as summarized above, name only Zeraoulia and Chojecki.

Acceptance. None documented. The site labels the problem OPEN, its page does not credit the result, and the claim's thread carries two comments with no recorded response from the site's curator. No journal record, arXiv posting or outside review is known here. The claim is therefore claimed.