Conjectures.io

Number theory

Erdős 68

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

References

No one has attempted this yet.

Formal statement

Lean type

True ↔ Irrational (∑' (n : ℕ), 1 / (↑(n + 2).factorial - 1))

What you must prove

import FormalConjectures.ErdosProblems.«68»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos68.erdos_68" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/68.lean

Source type SHA-256
sha256:b59291e94988a84176901a9e18e915d3dbc5c298f47b3a6b0a6e3c57d8b815b6
Task id
fc-379fc029-erdos68-erdos-68-5f01ac0cef-formalized-v1
Task commitment
sha256:a57fcecbed8bc93c73455dc8b342bb82f411023c8ad1079c328b6bc5526c025b

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.