Problem detail · source-aware
VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Every integer-valued strongly b-additive function g with gcd(g(1),…,g(b−1)) = 1 and nonnegative digit mean takes prime values at infinitely many primes, with a Mertens-type formula and normal-order results; the running example resolves the infinitude of OEIS A052034 (De Geest, 1999): infinitely many primes have a prime sum of squared decimal digits.
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.
Wrote most of the manuscript and the entire Lean 4 formalisation under the author's direction; the exposition was afterwards revised by the author and the same models. Numerical checks computed by machine; scripts distributed with the paper.
Provider: Anthropic · Prompt public: unknown · Independence: unknown
Lean-checked, and audited here on 26 August 2026 rather than taken on trust. Sixteen files, about 1550 lines, Lean 4.33.0: no sorry, no admit, no native_decide, and exactly one axiom declaration, confined to DigSq/Cited.lean as claimed. The committed axiom_audit.txt matches its own summary exactly - counted here as 32 results resting on Lean's three built-in axioms alone and 8 resting on those plus `mmr`, 40 in all, with the headline A052034_infinite in the second group. Cited.lean quotes Théorème 1 of Martin-Mauduit-Rivat in French verbatim and carries a quantifier-order note explaining that the encoding must be $\forall\varepsilon\,\exists C\,\forall x$, since $\forall x\,\exists C$ would make the axiom vacuous; that reasoning is correct and is the right thing to have worried about. The cited source is real (J. Inst. Math. Jussieu 18 (2019), 189-224) and the preprint the audit compares against resolves. Three limits, two of them volunteered by the repository itself. Only phases 1-2 are formalised: the Mertens formula, the counting bounds and the normal order are not. The axiom was compared against the preprint, not the paywalled published text. And the source was read by a model rather than a human, with the audit noting that its own §5 "exists because the first such reading was wrong". Lean was not compiled here, and axiom_audit.txt is labelled expected output rather than a captured transcript.
Correctness: supported · statement fidelity: unaudited · peer review: none
For every integer-valued strongly $b$-additive $g$ with $\gcd(g(1),\dots,g(b-1))=1$ and digit mean $\mu_g\ge0$: $g(p)$ is prime for infinitely many primes $p$. For $\mu_g>0$, $\sum 1/p$ over $p<X$ with $g(p)$ prime is $(d_g/\varphi(d_g))\log_3X + C_{g,1} + O(1/\log\log X)$, likewise for the first $j$ iterates. Also $\#\{p\le x: g(p)\text{ prime}\}\ll\pi(x)/\log\log x$, of that exact order on a large set of $x$, and $\omega(g(p))$ has normal order $\log_3 p$. What is new and what is not. For the digit sum $g=s_b$, Harman (2012) already proved both the infinitude and a Mertens formula; the new information there is the remainder tending to a limit rather than being $O(1)$, and the iterated version for $g=s$ is, in the paper's words, "contained, in a stronger and quantitative form, in Harman". The new content is the generalization to every such $g$, which delivers the running example $g=S$, the sum of squared decimal digits, and so the infinitude of OEIS A052034.
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.