Erdős problem 1063

Estimate $n_k$ by finding a better upper bound.

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1063.lean

Retained formal statement5 of 6

Monier observed that $n_k \le k!$ for $k \ge 3$ ([Mo85]). TODO: Find reference

FormalConjectures/ErdosProblems/1063.leanErdos1063.erdos_1063.variants.monier_upper_bound1 lineExact file

1∀ {k : ℕ}, 3 ≤ k → Erdos1063.n k ≤ k.factorial

SolvedStatement only, no proof