Counting squares with prescribed base-b digit sum

For base b≥2 and a prescribed large digit sum q, how many squares n² have that base-b digit sum with gcd(n,b)=1? Necessarily q is a square residue modulo b−1; for b=2 this restriction is automatic.

Why it matters and what counts as progress

Why it matters: Coprime roots prevent trivial trailing-zero padding, while quantitative counts strengthen mere existence.

What counts as progress: An all-base construction with explicit size and count bounds for every sufficiently large admissible q, treating the binary case separately.

How the problem developed

2005 · Recreational result [1]
R. K. Murthy and J. Ashbacher Recorded base-ten constructions of squares with admissible digital roots, establishing an existence observation without quantitative bounds across bases.
29 Aug 2026 · Quantitative theorem and formalization [2]
vibefrtz Reported that for each base b and every sufficiently large admissible q, exponentially many roots coprime to b give squares with digit sum q and a controlled size bound; the explicit existence/count bound is Lean-checked.

AI contribution

Local limits along squares and prime values of digital functions

For every base b≥2 and sufficiently large digit sum q congruent to a square modulo b−1 (automatic for b=2), the authors construct at least exp(c_b√q) squares n² of bounded size with gcd(n,b)=1 and base-b digit sum q. The explicit Lean statement gives q≥2304b⁴, n²≤b^(3q), and at least 2^(⌊√q/(36b)⌋) examples for b≥3, with a separate binary case.

AI involvementAI-centered

ImportanceNotable

Technical verificationFormal (Lean 4 / mathlib kernel + human)

Human understandingFull