---

Claim. The claim answers the main question of Problem 662 in the negative under each of the threshold readings it fixes: whether pairs at distance at most $t$ or at distance below $t$ are counted, and whether the count of a finite one-separated set is compared with the lattice neighbor count through the average degree or through the total number of pairs. The density of the triangular lattice is an asymptotic quantity, but the number of lattice points inside a single ball of fixed radius is not, and a slightly less dense lattice can place more points in one such ball. The witness is the lattice spanned by $u=(1,0)$ and $v=(136/305,273/305)$; since $|u|=|v|=1$ and $u\cdot v=136/305<1/2$, the basis is reduced, so the shortest nonzero lattice vectors have length $1$ and the lattice is one-separated, and it has $128$ nonzero vectors of length at most $6$ against the triangular lattice's $126$. On a $365\times365$ patch of this lattice, $n=133{,}225$ points, an exact count finds $268$ more ordered pairs at distance at most $6$ than $126n$, and far-separated copies of the patch give counterexamples with arbitrarily large $n$, so no cutoff "sufficiently large depending on $t$" rescues the inequality at $t=6$. Since the average number of neighbors within distance $6$ exceeds $126=f(6)$, some point has more than $f(6)$ such neighbors, so the closed-threshold count fails at $t=6$ counted over pairs, per point and on average: this refutes the printed question under each counting reading. A second lattice does the same at squared radius $300$ for the strict-threshold conjecture that Erdős states after the problem, in which the distances below the $n$th lattice distance $t_n$ are compared with $f(t_n)$. The claim also repairs the final clause, whose printed form asks whether a count is "less than $1$", and reports that the repaired question about distances below $\sqrt3$ has a positive answer; the repaired form is stated in the write-up and is not reproduced here.

Colin Snyder, posting under the forum account coffeewithcolin, submitted the claim to the site's proof-claims tab on 2026-07-15, with the write-up and a Lean 4 archive linked above; the posting reports that the statements are 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. The claim was submitted as a full proof claim. Against the problem's Statement, the site's wording, the closed-threshold counterexample is a full disproof; the strict-threshold conjecture and the repaired final clause are variants, recorded here and on the problem page and not counted.

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:

We claim the answer to the main question is no: the triangular lattice is not extremal for the number of distances $\le t$ among one-separated planar sets, under both the closed and strict threshold readings and both comparison conventions. The repaired particular question below $\sqrt{3}$ is true. All proved in Lean 4 / Mathlib, standard axioms only, no sorry, no native_decide. Idea: density is asymptotic, but finite-shell coordination is not, and a slightly less dense oblique lattice can fit more points in one particular ball. The one-separated rational lattice with basis $u=(1,0)$, $v=(136/305,273/305)$ has $128$ nonzero offsets at radius $6$ versus the triangular lattice's $126$; an exact count over a $365\times365$ patch ($n=133{,}225$) gives $268$ directed pairs above $126n$, and far-separated copies defeat every "sufficiently large" cutoff. A second lattice does the same for Erdős's stronger strict shell conjecture at squared radius $300$. Notes: The surviving problem text is corrupt (its sample values and final clause cannot be read literally), so we first recovered the primary 1997 source (Mathematica Japonica 46(3), via the National Diet Library of Japan; 28 overlapping OCR captures reconstructing 943 consecutive characters, hash-checked in the bundle) to fix the historical intent, then treated every remaining formula convention separately rather than choosing one. Patch counts are proved via injective incidence maps, not enumeration; small censuses use kernel decide. Verify: run check_answer/verify.sh (provenance hashes, both independent arithmetic audits, 8,570-job clean build); axiom print exactly [propext, Classical.choice, Quot.sound].

Depends on. No page of this wiki.

Acceptance. None documented. The site's label is open and the site's page does not credit the result. The proof-claims thread carries one objection, which disputes the claim's premise that the printed text of [Er97e] is corrupt; the claimant replied that the word meant only that the printed text cannot be read literally, which the problem page itself records, and credited the earlier repair note on the problem with the prior work. That dispute over the premise is unresolved. The write-up's National Diet Library OCR reconstruction (NDL PID 10996926, 943 consecutive characters of p. 532) reports that the 1997 text carries the same elements as the site's wording in the same order; the reconstruction is the claimant's and not a reading of the source by this corpus. The Lean archive is third-party Lean that this corpus has not built or audited, so it is a link and not evidence; its statements, the historical reconstruction and the build are not verified by the corpus. The claim is therefore claimed.