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
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.)
∀ (n p : ℕ), Nat.Prime p → p ≤ n → have k := n / p ^ Nat.log p n; p ∣ (Erdos291.a n).gcd (Erdos291.L n) ↔ ↑p ∣ (∑ i ∈ Finset.Icc 1 k, 1 / ↑i).num