Proved, on the site's label, which credits Gafni and Tao [GaTa25] for the affirmative answer: all but $O(X/(\log X)^2)$ of the prime gaps starting in $[X,2X]$ contain an integer whose least prime factor is at least the gap. A Lean proof of the statement in Alexeev's repository, not built here, is recorded beside the credit on the claim page (Gafni and Tao, 2025).