Erdős Problem 250

Reference: erdosproblems.com/250

theorem erdos_250 : (∀ (x : ℝ), HasSum (fun (n : ℕ) => ↑((ArithmeticFunction.sigma 1) n) / 2 ^ n) x → Irrational x) ↔ True

Is $$ \sum\frac{\sigma(n)}{2^n} $$ irrational? Here $\sigma(n)$ is the sum of divisors function.

The answer is yes, as shown by Nesterenko [Ne96].

[Ne96] Nesterenko, Yu V., Modular functions and transcendence questions, Mat. Sb. 187 9 (1996), 1319--1348.