Formal target: Corpus.OEIS78680.conjecture

There is a conjecture that the first zero is $n = 65536 = 2^{16}$ (which is equivalent to the statement that $2^{2^k} + 1$ is composite for $k > 4$).

Exact formal statement

And (Eq.{1} (Corpus.OEIS78680.a (HPow.hPow.{0, 0, 0} 2 16)) 0)
  (∀ (n : Nat), And (LE.le.{0} 1 n) (LT.lt.{0} n (HPow.hPow.{0, 0, 0} 2 16)) → Ne.{1} (Corpus.OEIS78680.a n) 0)

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record