VibeMathedMath problems solved with AI
Sign in

Prime values of digital functions along the primes

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.

Result
Proved(see note)
Status
Resolved
AI contribution
AI co-developed
Method
Argument
Field
Analytic number theory
Posed by
—
Year posed
1999
Years open
27y
Solved
2026-08
Model
Claude Opus 5, Claude Fable 5
Vendor
Anthropic
Collaborators
—
Verification
Lean-checked, statement unaudited
Publication
Preprint
Significance
11 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

For every integer-valued strongly bb-additive gg with gcd⁡(g(1),…,g(b−1))=1\gcd(g(1),\dots,g(b-1))=1 and digit mean μg≥0\mu_g\ge0: g(p)g(p) is prime for infinitely many primes pp. For μg>0\mu_g>0, ∑1/p\sum 1/p over p<Xp<X with g(p)g(p) prime is (dg/φ(dg))log⁡3X+Cg,1+O(1/log⁡log⁡X)(d_g/\varphi(d_g))\log_3X + C_{g,1} + O(1/\log\log X), likewise for the first jj iterates. Also #{p≤x:g(p) prime}≪π(x)/log⁡log⁡x\#\{p\le x: g(p)\text{ prime}\}\ll\pi(x)/\log\log x, of that exact order on a large set of xx, and ω(g(p))\omega(g(p)) has normal order log⁡3p\log_3 p.

What is new and what is not. For the digit sum g=sbg=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)O(1), and the iterated version for g=sg=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 gg, which delivers the running example g=Sg=S, the sum of squared decimal digits, and so the infinitude of OEIS A052034.

What the AI did

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.

Verification

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 ∀ε ∃C ∀x\forall\varepsilon\,\exists C\,\forall x, since ∀x ∃C\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.

Sources

Submitted by vibefrtz on

Changelog2 changes

Discussion