Erdős problem 259 · problems.science

Is $\sum_{n} \mu(n)^2\frac{n}{2^n}$ irrational?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

FormalConjectures/ErdosProblems/

259.lean

Retained formal statement1 of 1

Is $\sum_{n} \mu(n)^2\frac{n}{2^n}$ irrational?

This is true, and was proved by Chen and Ruzsa.

[ChRu99] Chen, Yong-Gao and Ruzsa, Imre Z., On the irrationality of certain series. Period. Math. Hungar. (1999), 31--37.

FormalConjectures/ErdosProblems/259.leanErdos259.erdos_2591 lineExact file

1Irrational (∑' (n : ℕ), ↑(ArithmeticFunction.moebius n) ^ 2 * ↑n / 2 ^ n)

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.