---

Claim. The answer to Problem 653 is yes: for every $\delta>0$ and every sufficiently large $n$ there is a set of $n$ points in the plane whose $n$ counts $R(x_i)$ of distinct distances to the other points take at least $(1-\delta)n$ different values, so $g(n)\ge(1-o(1))n$; with the trivial $g(n)\le n$ this gives $g(n)=(1-o(1))n$. The claimant is the solver recorded by the bounty site Conjectures.io under the name gus; the proof is a Lean 4 file of about 28,600 lines whose header names no author and no AI system, and which declares adapted material from the Prime Number Theorem and More project, ported to the pinned Lean and Mathlib under the Apache License 2.0. The AI system behind the proof, if any, is undisclosed. The record links an exposition of the proof, linked above, dated 17 September 2026 and written by Liam Kruer and Jensen Kohlmeyer, which says it was prepared by Conjectures with Codex assistance from the accepted Lean submission and that the site's Lean verification covers the formal source, not the prose. The result is known on the site's proof-claims tab through an entry of 27 September 2026, linked above, submitted by the site's curator, Thomas Bloom, naming conjectures.io as the claimant with the system recorded as Unknown; Bloom's note says that Bloom has not verified or examined the proof, posts the entry so that others are aware of it, does not endorse the Conjectures.io program, and objects that it is not transparent which AI system is used.

Submission note. Posted to erdosproblems.com as a proof claim by conjectures.io (account TFBloom) on 27 September 2026, giving "Unknown" as the AI used:

This formalisation claims a proof that $g(n)\geq (1-o(1))n$ always. Notes: This was posted on conjectures.io. I have not verified the proof yet, and do not claim that the formalisation is correct, nor have I looked into the proof at all. I am posting this here so that others are aware that this claim has been made, and we can discuss it here. This should also not be read as any kind of endorsement of the conjectures.io program - in my view it is using these problems, which it does not care about, for its own ends, without making any attempts to explain these proofs or engage with the mathematical community. It is also not transparent (e.g. of who is running these through the AI, how long for, and which AI).

The formal statement. The site attacked the formal-conjectures statement Erdos653.erdos_653 (FormalConjectures/ErdosProblems/653.lean at the catalog's commit of 2026-09-18) with its open answer fixed to true: there is a function $o$ with $o(n)\to0$ such that eventually $(1-o(n))\,n\le$ maximalDistinctDistancesFrom n, where the latter is the supremum, over $n$-point finite subsets $X$ of the Euclidean plane, of the number of distinct values of the per-point count of distinct distances from a point of $X$ to the points of $X$. That count includes the zero self-distance and so equals $R(x_i)+1$ for every point, which leaves the number of distinct values unchanged, and the proof file proves this equality; the ordering of the $R(x_i)$ in the problem's wording carries no content for that number; the supremum is a maximum since $g(n)\le n$; and the eventually-with-$o(n)\to0$ form is the asymptotic wording, finitely many $n$ being absorbable into $o$. So the formal statement is the problem's question clause for clause. The proof file's last declaration, target, spells that type out rather than naming the catalog theorem; the file's own Point, pinnedCount, diversity and Erdos653 live in a local namespace and are bridged to the catalog definition, and the file redefines no catalog or Mathlib name.

The construction. The points are $(2s)\times(2s)$ blocks of shifted integer grids whose rational offsets come from distinct primes congruent to $3$ modulo $4$, so that a point's count of distinct distances is governed by a coarse degree of its block and the blocks' counts fall into disjoint intervals; skew and jitter parameters spread the counts inside each block to a $(1-\delta)$ fraction of distinct values; a ported estimate for primes in arithmetic progressions feeds the sparsity bounds; and a padding step, adding a far point that shifts every count by one, reaches every $n$. The theorem target is discharged from official_target_of_squareFamilies applied to the construction squareFamilies. The exposition presents the same construction in another parametrization: $K=t^2$ blocks with $t=2(s+1)$, each an $L\times L$ grid, offset by Gaussian integers built from primes congruent to $3$ modulo $4$.

Acceptance. The reviewed evidence is the certification by Conjectures.io: the site's Lean kernel verified the submission, its review approved the record on 16 September 2026 under its policy v3, and the site certified the record on 17 September 2026 and paid the bounty. The site's review record says that the exact accepted proof and task passed its production verification, that the theorem establishes the intended asymptotic diversity of distance counts and that counting the self-distance does not alter it, that two independent agent assessments of the same model family, covering formal semantics and prior-source eligibility, agreed, and that no fresh replay was run on a second kernel, so its verdict rests on one kernel implementation; the permitted axioms were propext, Quot.sound and Classical.choice. That certification is the site's own and is the only outside acceptance recorded: no refereed publication exists, the erdosproblems.com page labels the problem OPEN (2026-10-07), and the formal-conjectures catalog marks the statement research open (commit of 2026-09-18, linked above). The corpus read the proof file as text and did not build it: a text scan found no sorry, axiom, native_decide, unsafe, implemented_by, extern, opaque or set_option outside doc comments and no instance or attribute registration; the target, header and key declarations were checked against the site's statement; and the finite lemmas on block degrees and the self-distance shift were recomputed independently in exact arithmetic. The kernel check is the site's, so the page lists no formalized evidence. Three limits of that reading stand: the statement file was compared at the catalog's commit of 2026-09-18, linked above, not at the commit the site pins; the file at that commit matches the site's printed statement apart from its open answer, and the site's own statement-hash check is the evidence that the pinned statement agrees; the shared definitions of the per-point count and its supremum were inferred from how the proof unfolds them rather than from their defining file; and the file's imports and namespace openings come from the site's trusted wrapper. A reported fidelity defect, a kernel rejection on replay or a reversal of the site's certification would return this claim to claimed.