Formal target: Corpus.OEIS5258.conjecture
For each $n = 1, 2, 3, \dots$ the polynomial $a_n(x) = \sum_{k=0}^n \binom{n}{k}^2 \binom{n+k}{k} x^k$ is irreducible over the field of rational numbers.
Exact formal statement
∀ (n : Nat), LE.le.{0} 1 n → Irreducible.{0} (Corpus.OEIS5258.aperyPoly n)This target is a formal statement, not a proof of the problem.
Environment availability: available.