Erdős problem 291
More generally, if the leading digit of in base is then . There is in fact a necessary and sufficient condition: a prime divides if and only if divides the numerator of , where is the leading digit of in base . This can be seen by writing and observing that the right-hand side is congruent to modulo . (The previous claim about follows immediately from Wolstenholme's theorem.)
Sources
FormalConjectures/ErdosProblems/
291.lean
Retained formal statement
Wu and Yan [WuYa22] have proved, conditional on being linearly independent over for any finite collection of primes (itself a consequence of Schanuel's conjecture), that the set of for which has upper density .
(LinearIndependent ℚ fun p => 1 / Real.log ↑↑p) → Filter.limsup (fun N => ↑↑{n ∈ Finset.Icc 1 N | (Erdos291.a n).gcd (Erdos291.L n) > 1}.card / ↑↑N) Filter.atTop = 1SolvedStatement only, no proof