Erdős problem 252
Erdős Problem 252: irrationality of the sum for a given .
Sources
FormalConjectures/ErdosProblems/
252.lean
Retained formal statement
∑ σ 1 n / n! is irrational. This is proved in [ErSt74].
Irrational (Erdos252.erdos_252_sum 1)SolvedStatement only, no proof