Formal target: Corpus.OEIS159829.conjecture2

Conjecture 2: For any $k \ge 3$, there are infinitely many primes of the form $n^k + m^k + 1$ for $n, m \ge 1$.

Exact formal statement

∀ (k : Nat),
  LE.le.{0} 3 k →
    Set.Infinite.{0}
      (Set.ofPred.{0} fun p =>
        Exists.{1} fun n =>
          Exists.{1} fun m =>
            And (LE.le.{0} 1 n)
              (And (LE.le.{0} 1 m)
                (And (Nat.Prime p)
                  (Eq.{1} p
                    (HAdd.hAdd.{0, 0, 0} (HAdd.hAdd.{0, 0, 0} (HPow.hPow.{0, 0, 0} n k) (HPow.hPow.{0, 0, 0} m k))
                      1)))))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record