Formal target: Corpus.WikipediaRudinsConjecture.rudins_conjecture

**Rudin's conjecture.** The maximal number of squares among the first $N$ terms of a non-trivial arithmetic progression grows at most like $\sqrt{N}$: $$Q(N) = O(\sqrt{N}).$$

Exact formal statement

Asymptotics.IsBigO.{0, 0, 0} Filter.atTop.{0} (fun N => Nat.cast.{0} (Corpus.WikipediaRudinsConjecture.Qmax N)) fun N =>
  (Nat.cast.{0} N).sqrt

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record