Formal target: Corpus.OEIS108866.conjecture

Conjecture: for $n > 3$, $\textrm{numerator}(-2/n + \sum_{k=1}^{n} \frac{2^k}{k}) == 0 (\textrm{mod} n^2)$ if and only if n is prime.

Exact formal statement

∀ {n : Nat},
  GT.gt.{0} n 3 →
    Iff ((HPow.hPow.{0, 0, 0} (Nat.cast.{0} n) 2).ModEq (Corpus.OEIS108866.ratExpression n).num 0) (Nat.Prime n)

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

Environment availability: available.