Erdős problem 394
For the least with , do the conjectured logarithmic-saving and adjacent-length estimates hold on average? Both answered affirmatively, with admissible in the bound.
Sources
FormalConjectures/ErdosProblems/
394.lean
Retained formal statement
The least positive multiple of n is n, so t 1 n = n.
∀ {n : ℕ}, 0 < n → Erdos394.t 1 n = nAPIStatement only, no proof