Erdős problem 202
Let with associated such that the congruence classes are disjoint (that is, every integer is for at most one ). How large can be in terms of ?
Sources
FormalConjectures/ErdosProblems/
202.lean
Retained formal statement
Let with associated such that the congruence classes are disjoint (that is, every integer is for at most one ). How large can be in terms of ?
Let be the maximum possible , and let .
This was proved by GPT-5.4 Pro (prompted by Ho Boon Suan), using the argument of [BFV13] together with the resolution of the Kahn-Kalai conjecture by Park and Pham [PaPh24], so that
∃ o, o =o[Filter.atTop] 1 ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ↑(Erdos202.f N) = ↑N * scaleL N ^ (-1 + o N)