Formal target: Corpus.OEIS38771.conjecture1
Conjecture: $\liminf_{n \to \infty} \frac{a(n)}{p_{n+1}^2} = 1 <$ $\limsup_{n \to \infty} \frac{a(n)}{p_{n+1}^2} = 2$.
Exact formal statement
have p_next_sq := fun n => HPow.hPow.{0, 0, 0} (Nat.cast.{0} (Nat.nth Nat.Prime n)) 2;
have seq := fun n => HDiv.hDiv.{0, 0, 0} (Nat.cast.{0} (Corpus.OEIS38771.a n)) (p_next_sq n);
And (Eq.{1} (Filter.liminf.{0, 0} seq Filter.atTop.{0}) 1) (Eq.{1} (Filter.limsup.{0, 0} seq Filter.atTop.{0}) 2)This target is a formal statement, not a proof of the problem.
Environment availability: available.