Formal target: Corpus.OEIS2426.conjecture

An integer $n > 3$ is prime if and only if $a(n) \equiv 1 \pmod{n^2}$.

Exact formal statement

∀ (n : Nat), LT.lt.{0} 3 n → Iff (Nat.Prime n) ((HPow.hPow.{0, 0, 0} n 2).ModEq (Corpus.OEIS2426.a n) 1)

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record