Formal target: Corpus.OEIS11545.conjecture1
Wolfgang Haken (1977) conjectured that no term of this sequence is a perfect square, and estimated the probability that this conjecture is false to be smaller than $10^-9$.
Exact formal statement
∀ (n : Nat), Not (IsSquare.{0} (Corpus.OEIS11545.a n))This target is a formal statement, not a proof of the problem.
Environment availability: available.