Formal target: Corpus.OEIS224.conjecture

$n^2 \equiv 1 \pmod{a(n)(a(n)-1)}$ if and only if $n$ is an odd prime.

Exact formal statement

∀ (n : Nat),
  LT.lt.{0} 1 n →
    Iff (And (Nat.Prime n) (Ne.{1} n 2))
      ((HMul.hMul.{0, 0, 0} (Corpus.OEIS224.a n) (HSub.hSub.{0, 0, 0} (Corpus.OEIS224.a n) 1)).ModEq
        (HPow.hPow.{0, 0, 0} n 2) 1)

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record