Formal target: Corpus.Erdos1101.erdos_1101.parts.i

1.

Exact formal statement

Not
  (Exists.{1} fun u =>
    And (Corpus.Erdos1101.IsGood u)
      (Exists.{1} fun k =>
        Asymptotics.IsBigO.{0, 0, 0} Filter.atTop.{0} (fun n => Nat.cast.{0} (u n)) fun n =>
          HPow.hPow.{0, 0, 0} (Nat.cast.{0} n) k))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record