Erdős problem 857

Estimate `m(n,k)`, or better give an asymptotic formula.

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

857.lean

Retained formal statement1 of 1

Estimate m(n,k), or better give an asymptotic formula.

FormalConjectures/ErdosProblems/857.leanErdos857.erdos_8572 linesExact file

1have f := sorry;2∀ (k : ℕ), 3 ≤ k → Filter.Tendsto (fun n => ↑(Erdos857.m n k) / f k n) Filter.atTop (nhds 1)

OpenStatement only, no proof