An Erdős–Kac law for palindromes and for reversed primes

This record contains the manuscript "An Erdős–Kac law for palindromes and for reversed primes" together with a Lean 4 formalisation certifying its deductive content. The paper. For every integer b ≥ 2 we determine the distribution of the number of prime factors, counted with or without multiplicity, of the base-b palindromes with λ digits and of the base-b reversals of the primes with λ digits: both obey an Erdős–Kac law with the classical centring log log b^λ and scaling √(log log b^λ). For the number of distinct prime factors we obtain in addition all moments of order up to ½(log log b^λ)^(1/3), uniformly in the order. For reversed primes the law persists when the leading digit of the prime is prescribed. The arithmetic inputs are a theorem of Col for palindromes and the Bombieri–Vinogradov theorem of Dartyge, Rivat and Swaenepoel for reversed primes; in both cases the excluded primes are those dividing b(b²−1). The deduction rests on the sieve-theoretic moment estimate of Granville and Soundararajan, cast as a general criterion in the manner of Murty, Murty and Pujahari and modified to allow a finite set of primes at which the local densities are arbitrary. The formalisation. The eight results quoted from the literature are declared as Lean 4 axioms, all of them in a single documented file, transcribed in the form in which the paper uses them. Every argument the paper itself makes is then proved in Lean from those axioms, with no "sorry". The Lean kernel therefore certifies the implication: if the eight quoted results hold as transcribed, then the paper's theorems hold. An axiom audit ("#print axioms" applied to each main theorem) is included, so that the exact logical dependencies of every theorem can be checked at a glance; in each case they coincide with the citations invoked by the corresponding proof in the paper. Two points lie outside the verification and are documented in the accompanying report: the transcriptions of the quoted results were cross-checked against their sources only to the extent recorded there, and the uniformity in the moment order is verified at each fixed order only — the case that the main theorems use. Contents. paper_anonymous.pdf is the manuscript. The archive additionally contains its LaTeX source, the Lean project (17 modules, pinned to Lean 4.33.0 and the matching Mathlib release), the axiom-audit driver together with its expected output, and VERIFICATION.md, which records the paper-to-Lean correspondence, the encoding conventions, the cross-checks of the axioms against the original sources, the two places where the formal proof deviates from the paper's equivalent argument, and an inventory of what is not machine-checked. Running "lake exe cache get && lake build" in the lean directory reproduces the check. Source repository: https://github.com/vibefrtz/vibemath The Lean sources are released under Apache-2.0; the manuscript is released under CC BY 4.0.