Formal target: Corpus.OEIS114362.conjecture1

Conjecture: if an integer $n > 1$ is odd, then $\zeta(2n)/\zeta(n)^2$ is irrational.

Exact formal statement

∀ (n : Nat),
  LT.lt.{0} 1 n →
    Odd.{0} n →
      Irrational
        (HDiv.hDiv.{0, 0, 0} (riemannZeta (HMul.hMul.{0, 0, 0} 2 (Nat.cast.{0} n)))
            (HPow.hPow.{0, 0, 0} (riemannZeta (Nat.cast.{0} n)) 2)).re

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record