Erdős problem 252
Erdős Problem 252: irrationality of the sum for a given .
Sources
FormalConjectures/ErdosProblems/
252.lean
Retained formal statement
Erdős Problem 252: irrationality of the sum for a given .
True ↔ ∀ k ≥ 1, Irrational (Erdos252.erdos_252_sum k)OpenStatement only, no proof