Erdős problem 624
Let be a finite set of size and be such that there is a function so that for every with we have . Prove that .
Sources
FormalConjectures/ErdosProblems/
624.lean
Retained formal statement
Let be a finite set of size and be such that there is a function so that for every with we have . Prove that .
Filter.Tendsto (fun n => ↑(Erdos624.H n) - Real.logb 2 ↑n) Filter.atTop Filter.atTopOpenStatement only, no proof