---

Claim. Two results on the multiplicities of the extreme distances of a finite planar set, from Wingate Jones's manuscript Second-largest and minimum distance multiplicities in planar point sets: an upper bound of 4/3, and related results on Erdős Problem #132 (2026). Write $\Delta$, $\Delta_2$ and $\delta$ for the largest, second-largest and smallest distances determined by an $n$-point set $A\subset\mathbb R^2$, $\mu(d)$ for the number of unordered pairs at distance $d$, $L_1$ and $L_2$ for the first two convex layers of $A$ and $m_3$ for the number of points of depth at least $3$.

1. Layer condition. Suppose every vertex of the convex hull of $A$ has at most three points of $A$ at distance $\Delta_2$ from it, which holds in particular when no four points of $A$ lie on a circle. Then $\mu(\Delta_2)\le\tfrac32|L_1|+|L_2|$, and the diameter and $\Delta_2$ each have multiplicity at most $n$ as soon as $|L_1|\le2m_3$, so the first question of Problem 132 has the answer yes for such sets. Theorem 1.3 of Clemen, Dumitrescu and Liu [CDL25] needs no hypothesis on the hull vertices and assumes $\min\{\tfrac32(|L_1|+|L_2|),\tfrac43|L_1|+2|L_2|,2|L_1|+|L_2|\}\le n$. Under the hypothesis above, the condition $|L_1|\le2m_3$, equivalently $\tfrac32|L_1|+|L_2|\le n$, follows from the first and third alternatives (the third is $|L_1|\le m_3$) but not from the second, so the result covers sets that theorem does not, as the manuscript's own remark says, without containing it.
2. The $4/3$ bound. For every $n$-point planar set, $\min\{\mu(\Delta_2),\mu(\delta)\}\le\tfrac43n+C_0$ for an absolute constant $C_0$. This bears on Problem 1.6 of [CDL25], which asks for the limit superior $L$ of $\max_{|A|=n}\min\{\mu(\Delta_2),\mu(\delta)\}/n$; the claimant gives the previous bounds as $9/7\le L\le3/2$, which the $4/3$ bound narrows to $9/7\le L\le4/3$: the lower bound is the construction posted in the problem's discussion thread on 25 July 2026 by ienjoymath (claim page), improving the published $9/8$ of Proposition 1.5 of [CDL25], and the upper one is Vesztergombi's inequality $\mu(\Delta_2)\le3n/2$ (vesztergombi_1987_large_distances_planar_sets).

The manuscript also reports, without formal verification, sharper bounds in most parameter ranges, at least three distances of multiplicity at most $n$ for convex sets with $6\le n\le18$ (the cases $n=7$, $11$ and $13$ by a SAT check inside Lean), and a linear number of such distances for almost cocircular convex sets.

Submission note. Posted to erdosproblems.com as a proof claim by Wingate Jones (account wingator) on 25 September 2026, giving "Claude Opus 5.5" as the AI used:

We prove two partial results related to Erdős Problem #132. (1) Layer condition, on the first question. Let $L_1, L_2$ be the first two convex layers of $A$ and $m_3$ the number of points of depth at least 3. If no vertex of the convex hull has four points of $A$ at the second-largest distance $\Delta_2$ (for example, if no four points are concyclic), then $\mu(\Delta_2)\le\frac32|L_1|+|L_2|$. So both the diameter and $\Delta_2$ occur at most $n$ times whenever $|L_1|\le 2m_3$. This extends Clemen–Dumitrescu–Liu's Theorem 1.3, which covers $|L_1|\le m_3$. (2) An upper bound of 4/3 for Clemen–Dumitrescu–Liu's Problem 1.6. For every $n$-point planar set, $\min\{\mu(\Delta_2),\mu(\delta)\}\le\frac43 n+C_0$, where $\delta$ is the minimum distance. The previous bounds were $9/7\le L\le 3/2$: the lower bound is ienjoymath's construction in the comments, and the upper bound is Vesztergombi's. Both are fully formalised in Lean 4 + Mathlib. Notes: This is a partial result. Neither question of #132 is resolved in general. Result (2) is about a related question of Clemen, Dumitrescu and Liu (arXiv:2505.04283, Problem 1.6). Formalisation. The formalisation is unconditional. The main theorems are Erdos132Main.erdos132_main43 (the $4/3$ bound; the earlier $15/11$ and $54/37$ bounds are also formalised) and the layer bound in E132Layer.lean. They have no sorry, and #print axioms reports only propext, Classical.choice and Quot.sound. The modules pass leanchecker. Vesztergombi's inequality $\mu(\Delta_2)\le\frac32 n$ and the Hopf–Pannwitz bound are proved inside the development, not assumed. The definitions of mult, dist2 and minDist are in Erdos132/E132MainDefs.lean. Further results in the PDF, not formally verified. Sharper bounds for most parameter ranges; at least three rare distances for convex sets with $6\le n\le 18$ ($n=7,11,13$ are in Lean via bv_decide; $n=15,17$ rely on DRAT certificates); a linear number of rare di

Covers. The first question for sets satisfying the layer condition of result 1, that is $|L_1|\le2m_3$ with no hull vertex seeing four points at distance $\Delta_2$; and the $4/3$ upper bound of result 2, which concerns a related quantity and is not one of the problem's questions. The manuscript also claims, without formal verification, a positive answer to the second question for sets in convex position with all but $w=o(n)$ of their points on one circle: such a set has at least $(n-3w+1)/4$ distances each occurring between one and $n$ times when $n\ge3w$ and $n+w\ge91$. Neither question of the problem is settled in general, as the claimant's own notes say.

Depends on. No page of this wiki. The Hopf–Pannwitz bound [HoPa34] and Vesztergombi's inequality are, by the claimant's account, proved inside the Lean development rather than assumed.

Claimant and postings. The claim was posted on the site's proof-claims tab on 25 September 2026 from the account wingator and is credited there to Wingate Jones, with the AI system named on the tab as Claude Opus 5.5; the repository's README names Claude (Anthropic) as the assistant used for exploration, computation, formalization and drafting. The manuscript (its version 3) and the Lean modules are linked above at the repository's revision of 25 September 2026, the code licensed Apache-2.0 and the paper CC BY 4.0. The README reports that the $4/3$ bound is the theorem Erdos132Main.erdos132_main43 (with the earlier bounds $15/11$ and $54/37$ also formalized, the constant $C_0=5\cdot10^9$ explicit), that the layer bound is in E132Layer.lean, that these have axiom closure propext, Classical.choice and Quot.sound and pass leanchecker, and that the convex cases $n=7$, $11$ and $13$ use bv_decide, whose compiler axiom the README discloses. None of this was built or audited by this corpus, so the page lists no formalized evidence.

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