Erdős Problem 68

Reference: erdosproblems.com/68

theorem Erdos68.erdos_68 : Irrational (∑' (n : ℕ), 1 / (↑(n + 2).factorial - 1)) ↔ sorry

Is $$\sum_{n=2}^\infty \frac{1}{n!-1}$$ irrational?

theorem Erdos68.sum_factorial_inv_eq_geometric : let f := fun (n k : ℕ) => 1 / ↑(n + 2).factorial ^ (k + 1); ∑' (n : ℕ), 1 / (↑(n + 2).factorial - 1) = ∑' (n : ℕ) (k : ℕ), f n k

$$\sum_{n=2}^\infty \frac{1}{n!-1} = \sum_{n=2}^\infty \sum_{k=1}^\infty \frac{1}{(n!)^k}$$