Formal target: Corpus.OEIS115257.conjecture
Conjecture: For any positive integer n, the polynomials Sum_{k=0}^n binomial(2k,k)^2*x^k and Sum_{k=0}^n binomial(2k,k)^2*x^k/(k+1) are irreducible over the field of rational numbers.
Exact formal statement
∀ (n : Nat),
LE.le.{0} 1 n → And (Irreducible.{0} (Corpus.OEIS115257.polyP n)) (Irreducible.{0} (Corpus.OEIS115257.polyQ n))This target is a formal statement, not a proof of the problem.
Environment availability: available.