Formal target: Corpus.Arxiv160908688SIncreasingrTuples.maximalLength_le_strong
$F(n) \leq n^{3/2}$.
Exact formal statement
∀ (n : Nat),
LE.le.{0} (Nat.cast.{0} (Corpus.Arxiv160908688SIncreasingrTuples.maximalLength n))
(HPow.hPow.{0, 0, 0} (Nat.cast.{0} n).sqrt 3)This target is a formal statement, not a proof of the problem.
Environment availability: available.