Local limits along squares and prime values of digital functions

Call an integer admissible if it is congruent to a square modulo b−1 (for b = 2 the condition is vacuous). For every base b ≥ 2 there are constants c_b, C_b > 0 such that the following holds: if q is sufficiently large and admissible, then

#{n ≥ 1 : (n,b) = 1, s_b(n²) = q, n² ≤ b^{C_b·q}} ≥ exp(c_b·√q).

The Lean 4 formalisation proves the explicit form: at least 2^{√q/(36b)} representations of size n² ≤ b^{3q} once q ≥ 2304·b⁴.

Result: Proved(see note)
Status: Resolved
AI contribution: AI co-developed
Method: Argument
Field: Digital problems; local limit theorems; Sidon sets; sieve methods
Posed by: Murthy–Ashbacher (base ten, recreational)
Year posed: 2005
Years open: 21y
Solved: 2026-08
Model: Claude Opus 5, Claude Fable 5, OpenAI Sol
Vendor: Anthropic, OpenAI
Collaborators: —
Verification: Lean-checked, statement unaudited
Publication: Preprint
Significance: 12 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

New theorems, not a formalisation of known results. In base ten the bare existence of a square with any admissible digit sum was recorded in the recreational literature (Murthy–Ashbacher 2005); the theorem here is the quantitative all-base version — roots coprime to b (excluding their trailing-zero trick), exp(c_b√q) representations of controlled size — and that statement is what is machine-checked, with effective but non-optimal constants. The same paper proves a local limit theorem for g(n²) for arbitrary digit weights in every base including binary, and sieves the values: level of distribution 1/2, P₃ and P₂ values, an unconditional Mertens-type prime-value law, a joint Erdős–Kac theorem. Caveats: the two shrinking-frequency estimates behind the local theorem enter the Lean development only as transcribed definitions; the sieve and asymptotic results are unformalised; Corollary 1.9 is formalised in bases 2 and 3 only; the analogous theory along squares of primes remains open.

What the AI did

Used at every stage: literature search, jointly working out the arguments, drafting the manuscript, and producing the Lean 4 formalisation with its axiom audit and validation scripts. The carry-free Sidon-set construction behind the submitted theorem and the paper's quantitative lattice local-limit framework were worked out jointly with the models, which also wrote most of the manuscript under the author's direction. The author verified all statements, proofs and references, made the final decisions on content and presentation, and is responsible for any remaining errors.

Verification

Lean-checked, and the development was audited here on 30 August 2026 rather than taken on the submitter's word. What was found matches the submission exactly.

33 files, 10,587 lines, with no $\texttt{sorry}$ , no $\texttt{admit}$ and no $\texttt{native\_decide}$ anywhere. Exactly two declared axioms exist in the whole project, both in $\texttt{DSS/Cited.lean}$ and both literature citations: Martin-Mauduit-Rivat and Halberstam-Heath-Brown-Richert. The committed $\texttt{axiom\_audit.txt}$ has 107 entries splitting 102 / 3 / 2 as claimed, and the five conditional ones are all the almost-prime $\texttt{p2\_count}$ and $\texttt{square\_p2}$ results - exactly where the paper says those inputs are used.

The submitted theorem is among the unconditional 102: $\texttt{DSS.sq\_digit\_sum\_count}$ depends only on $\texttt{propext}$ , $\texttt{Classical.choice}$ and $\texttt{Quot.sound}$ . Its statement was read against this entry's and matches term for term - $\texttt{sqSols}$ filters on coprimality to the base, $s_b(n^2)=q$ , and $n^2\le b^{3q}$ , with threshold $2304b^4$ and bound $2^{\lfloor\sqrt q/36b\rfloor}$ .

Not upgraded to Lean-verified, for one reason: it was not built. No Lean toolchain here, so every axiom closure above is read from the committed audit file rather than reproduced from $\texttt{lake build}$ . The kernel half is unconfirmed whatever the statement audit shows.

Sources

Related entries

ContinuesPrime values of digital functions

Submitted by vibefrtz on 29 Aug 2026