Local limits along squares and prime values of digital functions
resolvedconfidence 70%
VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
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⁴.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
Claude Opus 5, Claude Fable 5, OpenAI Sol
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.
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.
Local limits along squares and prime values of digital functions
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.
Known method families
argument (source-reported)
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.