Erdős problem 69
Is irrational? (Here counts the number of distinct prime divisors of .)
Sources
FormalConjectures/ErdosProblems/
69.lean
Retained formal statement
Tao observed that erdos_69 is a special case of erdos_257, since
have A := {n | Nat.Prime n};∑' (n : ℕ), ↑(ArithmeticFunction.cardDistinctFactors (n + 2)) / 2 ^ (n + 2) = ∑' (p : ↑A), 1 / (2 ^ ↑p - 1)SolvedStatement only, no proof