A Tilted Residue-Class Construction for Long Prime-Free Intervals claims Y(X) ≫ X log X / log₃ X and G(T) ≫ log T log₂ T / log₄ T.
After several hours of thought and conversations with Terry Tao and James Maynard, Ben Green wrote that he was more or less convinced by the claim; he also distinguished the existence of the Lean formalization from the remaining work of producing a readable human exposition.