---

Claim. Let $M(n)$ be the maximum, over all $n$-point sets $A\subset\mathbb R^2$, of the gap $f(d_1)-f(d_2)$ between the two largest distance multiplicities of $A$, the quantity Problem 959 asks to estimate. The claim is the lower bound

$$M(n)\ge n^{1+c/\log\log n}\qquad\text{with }c=\tfrac1{50000}$$

for all sufficiently large $n$, with ties among multiplicities counted as the write-up defines them and the maximum taken over every $n$-point set. The construction places normalized lattice disks, indexed by subsets of the primes congruent to $1$ modulo $4$, together with generically placed padding points, so that the normalized unit distance is realized with nearly the largest possible multiplicity while a reduced-denominator support argument suppresses every competing distance; the number of copies is chosen for each $n$, and a prime number theorem in arithmetic progressions, also formalized, supplies the asymptotics. The bound improves the $\Omega(n\log n)$ of Clemen, Dumitrescu and Liu, which the problem page cites as [CDL25]; the source card records it as Corollary 1.10 and records Problem 1.11, which asks whether it can be improved to $n^{1+c/\log\log n}$.

Colin Snyder, posting under the forum account coffeewithcolin, submitted the claim to the site's proof-claims tab on 2026-07-15 as a full claim, with the write-up and a Lean 4 archive linked above. A comment on the thread noted that no matching upper bound is claimed; the claimant agreed and asked for reclassification, and a moderator changed the claim to a partial claim. The posting reports that the theorem Erdos959.erdos959_superlinear_lower_bound is proved in Lean 4 over Mathlib with the standard axioms only, without sorry or native_decide, and names GPT 5.6 (custom harness) as the system used.

Submission note. Posted to erdosproblems.com as a proof claim by Colin Snyder (account coffeewithcolin) on 15 July 2026, giving "GPT 5.6 (custom harness)" as the AI used:

Let $M(n)$ be the maximum over all $n$-point sets $A\subset\mathbb{R}^2$ of the gap $f(d_1)-f(d_2)$ between the top two distance multiplicities. We claim the explicit superlinear lower bound: with $c=1/50000$, for all sufficiently large $n$, [M(n)\ge n^{1+c/\log\log n}.] The previous best was $\Omega(n\log n)$. Proved in Lean 4 / Mathlib (theorem Erdos959.erdos959_superlinear_lower_bound), standard axioms only, no sorry, no native_decide. Idea: build normalized replicated lattice disks indexed by subsets of the primes $\equiv 1 \pmod 4$, so one distance (the normalized unit) is realized with near-maximal multiplicity, while every competing distance is suppressed by a reduced-denominator support argument. Blocks and padding points are placed generically, replication is chosen adaptively for each $n$, and a formalized prime number theorem in arithmetic progressions supplies the asymptotics. The formal gap semantics include ties and take the true maximum over all $n$-point sets Notes: Honestly scoped: no matching upper bound or exact order is claimed. The PNT-in-APs input is a pinned sorry-free fork of the community PrimeNumberTheoremAnd library. Two trivial native_decide certificates (both "Nat.totient 4 = 2") were replaced with kernel decide after refereeing; the pinned verifier re-ran PASS. Verify: run check_answer/verify.sh (8,624 jobs); "#print axioms" on the final theorem gives exactly [propext, Classical.choice, Quot.sound].

Covers. A lower bound on $M(n)$ of order $n^{1+c/\log\log n}$ for large $n$. The problem asks for an estimate of $M(n)$; no upper bound is claimed, and the order of $M(n)$ remains open.

Depends on. No page of this wiki.

Acceptance. None documented. The site's label was OPEN on 2026-10-06, the proof-claims thread carries only the reclassification exchange described above, and the site's page does not credit the result. The formal-conjectures statement file for the problem has carried, since 2026-08-07 (the record link above is pinned at the catalog's commit of that day), a companion statement erdos_959.lower_bound, the existence of $c>0$ with $n^{1+c/\log\log n}\leq M(n)$ for all large $n$, marked research solved with a formal_proof attribute pointing at the theorem erdos959_superlinear_lower_bound in Research/FinalLowerBound.lean of the starfleet/erdos-959 folder of the williamjblair/lean-proofs repository, linked above at that revision; the folder's README says its hosted developments are Star Fleet Math's, Colin Snyder's, proofs, and the theorem name and the constant $c=1/50000$ match this posting. The hosted project depends on Mathlib and on the PrimeNumberTheoremAnd library. The archive and the hosted file are third-party Lean that this corpus has not built or audited, so they are links and not evidence. A second claim, posted six days later, asserts a stronger bound by a different construction and has its own claim page. The claim is therefore claimed.