Formal target: Corpus.Erdos535.erdos_535

Let $r \geq 3$, and let $f_r(N)$ denote the size of the largest subset of $\{1,\ldots,N\}$ such that no subset of size $r$ has the same pairwise greatest common divisor between all elements.

Exact formal statement

∀ (r : Nat),
  GE.ge.{0} r 3 →
    Exists.{1} fun c =>
      And (GT.gt.{0} c 0)
        (Filter.Eventually.{0}
          (fun N =>
            LE.le.{0} (Nat.cast.{0} (Corpus.Erdos535.f r N))
              (HPow.hPow.{0, 0, 0} (Nat.cast.{0} N) (HDiv.hDiv.{0, 0, 0} c (Real.log (Real.log (Nat.cast.{0} N))))))
          Filter.atTop.{0})

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record