Formal target: Corpus.OEIS105720.conjecture

Terms are squares at only(?) three values of $n = 3, 6, 4072$: corresponding terms are 6^2, 13^2, and 15735^2.

Exact formal statement

∀ (n : Nat),
  LT.lt.{0} 0 n → Iff (IsSquare.{0} (Corpus.OEIS105720.a n)) (Or (Eq.{1} n 3) (Or (Eq.{1} n 6) (Eq.{1} n 4072)))

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

Environment availability: available.