Erdős problem 249

Is $\sum_{n} \frac{\phi(n)}{2^n}$ irrational? Here $\phi$ is the Euler totient function.

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

249.lean

Retained formal statement1 of 1

Is $\sum_{n} \frac{\phi(n)}{2^n}$ irrational? Here $\phi$ is the Euler totient function.

FormalConjectures/ErdosProblems/249.leanErdos249.erdos_2491 lineExact file

1True ↔ Irrational (∑' (n : ℕ), ↑n.totient / 2 ^ n)

OpenStatement only, no proof