Formal target: Corpus.OEIS83753.conjecture

There are no palindromic numbers greater than 1 which are the fifth or higher power of a natural number.

Exact formal statement

∀ (m k : Nat),
  LT.lt.{0} 1 m →
    Corpus.OEIS83753.IsDecimalPalindrome m →
      LE.le.{0} 5 k → Not (Exists.{1} fun x => Eq.{1} m (HPow.hPow.{0, 0, 0} x k))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record