The board / covering systems / #202
Erdős Problem #202
SOLVED LEANdatabase updated 2026-05-14
Resolved in some way other than a straight proof or disproof — usual for open-ended questions, or for multi-part problems whose parts went different ways. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
`f N` is the maximum possible `r` such that there are moduli \(n_1<\cdots<n_r\leq N\) with associated residues \(a_i\pmod{n_i}\) whose congruence classes are disjoint.
Let \(n_1<\cdots < n_r\leq N\) with associated \(a_i\pmod{n_i}\) such that the congruence classes are disjoint (that is, every integer is \(\equiv a_i\pmod{n_i}\) for at most one \(1\leq i\leq r\)). How large can \(r\) be in terms of \(N\)? Let \(f(N)\) be the maximum possible \(r\), and let \(L(N)=\exp(\sqrt{\log N\log\log N})\). 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 \[f(N)= N L(N)^{-1+o(1)}.\]
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/202.Prizenone
Topicscovering systems
Statement in LeanFormal Conjectures
Solution in Leanyes
OEISA389975
Original pageerdosproblems.com/202
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.