Formal target: Corpus.OEIS1146.conjecture

I conjecture that { $a(n)$ ; $n>1$ } are the numbers such that $n^4-1$ divides $2^n-1$, intersection of A247219 and A247165.

Exact formal statement

∀ (k : Nat),
  Dvd.dvd.{0} (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} k 4) 1) (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 k) 1) →
    GT.gt.{0} k 1 → Exists.{1} fun n => And (LE.le.{0} 2 n) (Eq.{1} k (Corpus.OEIS1146.a n))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record