Are there infinitely many n with ω(n−k) < (1+ε)·log k/log log k for all large k? (Erdős #679)

Let $\epsilon>0$ and let $\omega(n)$ denote the number of distinct prime factors of $n$. Are there infinitely many integers $n$ such that $$\omega(n-k) < (1+\epsilon)\frac{\log k}{\log\log k}$$ for all $k<n$ that are sufficiently large depending only on $\epsilon$? Erdős also asked the sharper question of whether one can show that the stronger bound $$\omega(n-k) < \frac{\log k}{\log\log k} + O(1)$$ (holding for all large $k<n$, for infinitely many $n$) is false. The analogous questions may be posed for $\Omega(n)$, the number of prime factors counted with multiplicity, with $\log k/\log\log k$ replaced by $\log_2 k$.

Acceptance. This is an OPEN, proof-shaped problem. FULLY RESOLVES: a complete proof — machine-checkable (Lean/Coq) preferred, otherwise a full written proof — that settles the main question, i.e. either establishes that for every fixed $\epsilon>0$ there are infinitely many $n$ with $\omega(n-k)<(1+\epsilon)\log k/\log\log k$ for all sufficiently large $k<n$, or proves that no such infinite family exists for some $\epsilon>0$ (the negative answer conjectured by Lau). ADVANCES: prove a strict improvement over the frontier stated in the background — for instance, reduce the constant $C$ in Lau's bound $\omega(n-k)\leq\Omega(n-k)\leq C\log k$ (for infinitely many $n$, all $1<k<n$), or determine the true order of $\min_n\max_{k<n}\omega(n-k)$, or resolve the $\Omega$-analogue — each with a proof. A reproducible computational search over $n$ with a verifiable certificate is a valid supporting contribution but cannot by itself close a proof-shaped question. Deliver a proof (formal or written), or the improved-bound proof, or a search program plus certificate.