---

Claim. The answer to Problem 90 is no, with the exponent $1.043171$. Theorem 1.1 of Eric Naslund, An Exponent of 1.043 for the Unit Distance Problem, dated 8 October 2026 in the author's repository, states that there are finite sets $U_j\subset\mathbb R^2$ with $|U_j|\to\infty$ and

$$\frac{u(U_j)}{|U_j|^{1.043171}}\to\infty,$$

where $u(U)$ counts the unordered pairs of points of $U$ at Euclidean distance one; in particular $u(n)\ge n^{1.043171}$ for arbitrarily large $n$ (p. 1). The first preprint link is the version of 8 October that the registry entry cites, and the second its revision of 9 October (101 pages), which this page was read against; Theorem 1.1 is the same in both, and the page numbers here are the revision's. A fixed positive gain along an unbounded sequence of $n$ exceeds $C/\log\log n$ for every fixed $C$ once $n$ is large, so the bound the problem asks about fails. The theorem asserts nothing for every large $n$.

The paper says the proof uses no unproved hypothesis, such as the generalized Riemann hypothesis, but is computer-assisted (p. 2): finite facts about the tower, a census of primes up to norm $4\cdot10^{13}$ (Proposition 5.12, p. 48), rigorous enclosures of 576 $L$-functions of degrees 4 and 8 at 21 real points near $1$ (Proposition 6.5, p. 58) and the final margin at $\delta=0.043171$ (Section 11, pp. 84--89) are certified by exact computation and interval arithmetic in supplementary programs in the repository. A replay program reruns the certificate (Subsection 1.8, p. 8) with two limits: it recomputes the $L$-values at three of the abscissae and checks the others against their stored hashes, and it repeats the census only on sample ranges, checking the census bins against an independent classification. The construction is the number-field method of OpenAI and Sawin, with unit distances from elements of relative norm one in quadratic extensions $K/F$ where $F$ has both real and complex places; the fields come from an infinite pro-$2$ tower over $\mathbb Q(\sqrt{241})$ ramified only above $2$, $3$ and $5$, with Frobenius conditions at the two primes above $29$ and at one prime above $41$. The relative zeta value is bounded by $C_{\rm eff}=0.0422764$ (Theorem 4.2, p. 32) through the dihedral quotients of the tower group and a field $E_{W''}$ of degree $8192$ contained in every field of the tower. Table 1 of the revision (p. 2) lists the exponents claimed between Sawin's $1.014114$ and its own, the largest being the author's unpublished $1.0358324$. The version of 8 October instead names as the largest exponent previously claimed the author's earlier manuscript An Exponent of 1.04273 for the Unit Distance Problem, in the same repository, and says it keeps that manuscript's method and most of its construction; the revision drops the citation and sets aside only "preliminary versions of the present work". The paper's AI Methodology statement says that agents developed the mathematics, wrote the programs and wrote the paper under the author's supervision: Claude Opus 5.5 in Claude Code produced the refinements of the zeta bound, the certificates and the paper, an agent run of the Muse Spark system found the Frobenius condition above $41$, and the preliminary versions were produced with Claude Opus 5.5, ChatGPT Sol 5.6 and ChatGPT Astra 6.

Submission note. The Palomar registry's description of entry PALOMAR-2026-10-01-000018, version 2, registered on 10 October 2026 by its maintainer Eric Naslund:

Lean formalization accompanying the paper An Exponent of 1.043 for the Unit Distance Problem by Eric Naslund (cited under sources), which proves the exponent 1.043171 unconditionally with a computer-assisted certificate. Conditional theorem on unit distances in the Euclidean plane. Let B = Q(sqrt 241) and let E be the number field of degree 512 generated over Q by sqrt 241 and square roots of the eight elements -1, -71011068 + 4574225 sqrt 241, (-6101 - 393 sqrt 241)/2, (6101 - 393 sqrt 241)/2, 31 - 2 sqrt 241, 31 + 2 sqrt 241, 326 - 21 sqrt 241 and 326 + 21 sqrt 241 of B (a basis of the {2,3,5}-units of B modulo squares). Let E_W be the field of degree 8192 obtained from E by adjoining square roots of four explicit elements beta_1, ..., beta_4 of E, each generating with two of the square roots a dihedral extension of B of degree 8 (the elements are written out in the Challenge). Hypothesis (H_W) is one displayed numerical inequality for the Dedekind zeta function of E_W: log(Re zeta_{E_W}(1 + 1/4411))/8192 + (1/4411)((L - gamma - log(4 pi))/4 - Re((zeta_{E_W}'/zeta_{E_W})(2))/8192) < 50969/1000000, where L = (9/4) log 2 + (1/2) log 3615 and gamma is Euler's constant. The compared theorem proves that (H_W) implies the existence of finite sets U_j in the plane with |U_j| -> infinity such that the number of unordered pairs of points of U_j at distance one, divided by |U_j|^(20863/20000), tends to infinity. The exponent is exactly 20863/20000 = 1.04315. The conclusion is a sequence statement only; no bound at every sufficiently large cardinality is asserted. The infinite pro-2 tower over B with Frobenius caps at both primes above 29 and at one prime above 41 (generators, relation bound, presentation, Golod-Shafarevich infinitude, local data), its fields, which are Galois over B and over a fixed base field but not over Q, their local types and signature, the root-discriminant bound, the field E_W with its degree, its embedding in the base field and its local data, the passage from (H_W) to the analytic ceiling, the numerical margin and the planar construction are proved in Lean over Mathlib; (H_W) itself is not proved. Outside Lean, a rigorous computation (certified values of the 576 L-functions of degrees 4 and 8 in the factorization of zeta_{E_W} and an Euler product with explicit tail) bounds the left side of (H_W) by 0.0509172; that computation is not part of the formal proof. The earlier formalization registered as PALOMAR-2026-10-01-000018 version 1 proved the exponent 10427/10000 from a different inequality, for the field E.

Depends on. No page of this wiki. The paper calls itself self-contained apart from the standard results it cites, among them the Golod--Shafarevich criterion, and its supplementary programs, which import programs of the author's earlier manuscripts in the same repository.

Formalization. The registry's selected theorem UnitDistanceSqrt241Submission.target_of_wide_zeta_bound, in the 158-line challenge file lean/ChallengeZeta241.lean at the pinned commit, which imports only Mathlib, proves a weaker, conditional form of Theorem 1.1: if

$$\frac{\log\operatorname{Re}\zeta_{E_W}\bigl(1+\tfrac1{4411}\bigr)}{8192} +\frac1{4411}\Bigl(\frac{\ell-\gamma-\log(4\pi)}4 -\frac{\operatorname{Re}(\zeta_{E_W}'/\zeta_{E_W})(2)}{8192}\Bigr) <0.050969,$$

with $\ell=\tfrac94\log2+\tfrac12\log3615$, $\gamma$ Euler's constant and $E_W$ the field of degree $8192$ written out in the challenge file (the paper's $E_{W''}$), then there are finite sets $U_j\subset\mathbb C$ with $|U_j|\to\infty$ and the number of unordered pairs at distance one in $U_j$, divided by $|U_j|^{1.04315}$, tending to infinity. Under that inequality, $(H_W)$, the Lean theorem disproves the problem's bound with the exponent $1.04315$. $(H_W)$ is not proved in Lean: the paper's Remark 4.38 (pp. 43--44) says that a supplementary program bounds its left side by $0.0509172$ from the enclosures of Proposition 6.5, and that the formalization does not cover the census beyond norm $1000$, the signed kernel or the general shell weights. Its Status subsection (Subsection 1.5, p. 6) concludes that the formalization does not prove Theorem 1.1, even conditionally. The registry entry records Lean v4.35.0-rc2, the Mathlib revision it pins, the permitted axioms propext, Quot.sound and Classical.choice, checks by two further kernels, and an automated review by a language model with a neutral outcome and no warnings; the project's metadata reports no sorry and no native_decide, gives its review status as self-assessed, and says the Lean was produced with AI tools, Claude Opus 5.5 in Claude Code and Codex, under the author's direction. Version 1 of the entry, registered on 1 October 2026 (record), proved the exponent $1.0427$ from a different inequality for the Kummer field $E$ of degree $512$, alongside the 1.04273 manuscript. This corpus has neither built nor audited the development, and no statement-fidelity review of its challenge file exists here, so it gives no formalized evidence.

Acceptance. None documented. The paper is not refereed and is not on arXiv. Its Status subsection (p. 6) reports ten fresh-context reviews of the dihedral refinements, the signed kernel, the shell weights and the intermediate certificates, one of which found a corrected error in an intermediate certificate, and three of the whole manuscript, all by AI agents and not human peer review; it says that no reviewer recomputed the octic $L$-values and that the finite computations for the cap above $41$ have had no full independent review. The corpus has not replayed the certificate. The claim is therefore claimed; the problem's standing rests on OpenAI's accepted claim and does not change.