A published paper or arXiv preprint answers the main question of Erdős Problem #486 (theorem erdos_486 in formal-conjectures) in full (proof, disproof, or the exact value asked for) with no hypotheses beyond the problem's own.

The problem, as stated in formal-conjectures (Apache 2.0):

Let A \subseteq \mathbb{N}, and for each n \in A choose some X_n \subseteq \mathbb{Z}/n\mathbb{Z}. Let B = \{m \in \mathbb{N} : m \not\in X_n \pmod{n} \text{ for all } n \in A \text{ with } m > n\}. Must B have a logarithmic density? The set A is encoded by taking X_n = \emptyset for n \notin A. Only positive moduli n are considered, since \mathbb{Z}/0\mathbb{Z} = \mathbb{Z} would allow B to be an arbitrary set. The answer is no: Wang [Wa26] (with GPT-5.6) constructed a congruence system whose survivor set B has lower logarithmic density at most 177/200 and upper logarithmic density at least 49/50. The first linked formal proof establishes this for the real-cutoff normalisation \frac{1}{\log x}\sum_{m < x, m \in B} \frac{1}{m} with the moduli restricted to A; the second derives the statement below (`Set.HasLogDensity`, all moduli) from it.