Skip to content

Erdős problem 252

Start work

Erdős Problem 252: irrationality of the sum for a given kk.

Sources

The source's own material, retained exactly.

9 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

252.lean

Retained formal statement9 of 9

If Schinzel's conjecture is true, then ∑ σ k n / n! is irrational for all k. This is proved in [ScPu06].

FormalConjectures/ErdosProblems/252.leanErdos252.erdos_252.variants.schinzel4 linesExact file
(∀ (fs : Finset (Polynomial ℤ)),    (∀ f ∈ fs, BunyakovskyCondition f) →      SchinzelCondition fs → Infinite ↑{n | ∀ f ∈ fs, Prime (Polynomial.eval n f).natAbs}) →  ∀ (k : ℕ), Irrational (Erdos252.erdos_252_sum k)
SolvedStatement only, no proof