---

Claim. The answer to Problem 486 is no. Theorem 1.1 of S. Wang, A Proposed Solution to Erdős Problem 486 (10 pages, hosted in the author's GitHub repository; first posted on 16 July 2026, last changed on 22 July 2026, and linked above at the repository's commit of 2 August 2026) asserts that there are a fixed infinite $A\subseteq\mathbb N$ and fixed $X_n\subseteq\mathbb Z/n\mathbb Z$ for $n\in A$ such that the survivor set $B$ of the statement satisfies

$$\liminf_{x\to\infty}\frac1{\log x}\sum_{\substack{m<x\\m\in B}}\frac1m \leq\frac{177}{200} <\frac{49}{50} \leq\limsup_{x\to\infty}\frac1{\log x}\sum_{\substack{m<x\\m\in B}}\frac1m,$$

so that $B$ has no logarithmic density. The corpus's card for the manuscript is wang_2026_proposed_solution_erdos_problem_486.

Submission note. Posted to erdosproblems.com as a proof claim by Shouqiao Wang (account ShouqiaoWang) on 16 July 2026, giving "GPT-5.6 Sol" as the AI used:

The answer is no: the logarithmic density does not always exist. The idea is to add groups of congruence conditions at larger and larger scales. When a group first becomes active, it removes enough integers to push the logarithmic average down. But in the long run, the residue classes used by that group cover only a very small proportion of the integers. We place many groups close together to make the average fall, and then leave a very long gap so that the average can rise again, while the later groups are still inactive. Repeating this gives one fixed construction in which the logarithmic average keeps moving between two different levels, so it does not converge. Notes: This proposed solution was found through my AI pipeline and was generated almost entirely by GPT-5.6 Sol. I have personally read and checked the proof, and I believe it is correct.

Argument, as the claimant describes it. Finite groups of congruence conditions are installed at larger and larger dyadic scales. A probabilistic construction (Lemmas 3.1–3.4) gives, at each large scale $Q=2^j$, moduli $q$ between $19Q/20$ and $21Q/20$ and residue sets $X_q$ that delete a fixed share of the integers in $[11Q/10,19Q/10]$ as soon as they become active, while the Haar measure of the completed periodic footprint of those classes is summably small. Runs of such blocks are placed close together to pull the logarithmic average down, and a recovery lemma (Lemma 2.1), which gives the logarithmic density of the survivor set of any finite system as one minus the measure of its residue cylinders, lets a long gap bring the average back up before the next run, whose moduli are still inactive. The two subsequences give the liminf and limsup bounds. Remark 1.2 observes that replacing the strict activation $n<m$ by $n\leq m$ changes $B$ by a primitive set, which by Behrend's theorem has logarithmic density zero. The manuscript places the construction outside the summable regime $\sum_{n\in A}|X_n|/n<\infty$ of Araújo's positive theorem, since every installed scale contributes a fixed positive amount to that sum (Section 1, Remark 4.1). With many residues per modulus, the construction also lies outside the zero-residue case $X_n=\{0\}$ of Davenport and Erdős, recorded on its own claim page.

Claimant. Shouqiao Wang, whose title page gives the affiliations Columbia University and Multiscalar Intelligence. The tab's submission says the claim was produced using an AI system, GPT-5.6 Sol, and its notes say the solution was generated almost entirely by GPT-5.6 Sol through the author's pipeline and that the author read and checked the proof; the manuscript's abstract says the proposed solution was found by GPT-5.6. The repository carries an MIT license for the repository as a whole.

Formal verification by the author and others. The author posted a Lean 4 development in the same repository on 17 July 2026, linked above at the pinned commit, whose top-level theorem erdos486_negative is stated as the negation of the problem's assertion with the strict activation condition $m>n$; in the claim's thread Wang reports that it compiles with Lean 4.27.0 and Mathlib with no sorry and no axioms beyond the standard ones. A forum commenter reported on 2 August 2026 a kernel replay of the development from a cleared build tree, with #print axioms on erdos486_negative giving only propext, Classical.choice and Quot.sound. Boris Alexeev's repository of formalized Erdős problems holds a file, linked above at a pinned commit, whose header calls it a Lean 4.33.0 port of Wang's formalization of the negative answer; it is a formalization link on this page, not a result of its own. Since 18 September 2026 the formal-conjectures statement of the problem has been tagged research solved, crediting Wang, with two formal proofs linked: Alexeev's port and a fork of formal-conjectures, linked above at a pinned commit, which carries Wang's development through Alexeev's port, with its license and attribution kept, and adds a bridge module deriving the catalog's statement from it. This corpus has built and audited none of these developments, so no formalized evidence is listed.

Standing. Claimed, full. The claim was submitted to the site's proof-claims tab on 16 July 2026 as a full proof. The site's curator, Thomas Bloom, wrote in the tab's thread the same day that Bloom had not checked the proof in detail, that its statement and strategy seemed plausible, and that for a delicate quantitative construction Bloom would wait for a formalized version rather than check it line by line; that comment is not an acceptance. The commenter's kernel replay is not a review by a named reviewer. The site labels the problem OPEN (2026-10-06), its commentary (last edited 8 April 2026) does not mention the manuscript, and no arXiv version, refereed publication or independent review of the argument is recorded.

Depends on. No page of this wiki.