Erdős problem 389
Is it true that for every there is a such that
Sources
FormalConjectures/ErdosProblems/
389.lean
Retained formal statement
Bhavik Mehta has computed the minimal such for . For example, the minimal for is .
IsLeast {k | 1 ≤ k ∧ ∏ i ∈ Finset.range k, (4 + i) ∣ ∏ i ∈ Finset.range k, (4 + k + i)} 207TextbookStatement only, no proof