Formal target: Corpus.Erdos409.erdos_409.variants.sigma_termination

If $n > 1$ then the iteration $n\mapsto\sigma(n) - 1$ necessarily reaches a prime.

Exact formal statement

∀ (n : Nat),
  GT.gt.{0} n 1 →
    Exists.{1} fun i =>
      Nat.Prime
        (Nat.iterate.{1} (fun x => HSub.hSub.{0, 0, 0} (DFunLike.coe.{1, 1, 1} (ArithmeticFunction.sigma 1) x) 1) i n)

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record