---

Let $A$ be the set of positive integers whose binary expansion has nonzero digits only in even places and $B$ the set with nonzero digits only in odd places. Both have $\gg N^{1/2}$ elements up to $N$ for all large $N$, and every $n \geq 1$ has at most one representation $n = a + b$ with $a \in A$ and $b \in B$, since the two sets of digit positions are disjoint (exactly one when $0$ is admitted to both sets, as the site's remark counts, since the positions then also cover every $n$). If $a_1 - a_2 = b_1 - b_2$ with $a_1, a_2 \in A$ and $b_1, b_2 \in B$ then $a_1 + b_2 = a_2 + b_1$, and the uniqueness gives $a_1 = a_2$ and $b_1 = b_2$, so there is no solution with nonzero difference and the answer to Problem 331 is no. Ruzsa communicated the counterexample to the site. The same counterexample was published in 1984 by Erdős and Freud (J. Number Theory 18, 99--109), who quote the question from the 1980 monograph and answer it with the integers using only even, respectively only odd, powers of two, without crediting Ruzsa; that publication has its own claim page. The site also records Ruzsa's suggested variant, which asks the same question under the stronger hypothesis $\lvert A \cap \{1, \ldots, N\} \rvert \sim c_A N^{1/2}$ and likewise for $B$; that variant is not the problem's question. Theorem 4 of Erdős and Freud answers it yes: when $\liminf \min\{A(x), B(x)\} / \sqrt x > 0$ and the equation has only trivial solutions, neither $A(x) / \sqrt x$ nor $B(x) / \sqrt x$ tends to a limit, so sets with the asymptotics of the variant cannot have only finitely many nontrivial solutions: removing the finitely many elements of $A$ involved in them would leave sets with the same asymptotics and none. The formal-conjectures statement file records that reading at its revision of 30 September 2026 (linked above), marking the variant erdos_331.variants.ruzsa solved in the affirmative with the paper as its source.

Acceptance. Reviewed: the site's curator, Thomas Bloom, labels the problem disproved on erdosproblems.com, states the counterexample in the page's commentary with the remark that it is easily checked, and thanks Ruzsa for it; the curator's acceptance is the documented acceptance. The remark is not dated on the site; its earliest documented appearance is the Wayback Machine's snapshot of the problem page of 2024-06-19, which already carries the remark, the variant, the thanks to Ruzsa and the solved label, and the page is dated to that snapshot.

Formalization. The site's label carries a Lean mark. It refers to a Lean 4 formalization of Ruzsa's counterexample that Wouter van Doorn posted in the site's discussion thread on 2026-01-31, written with the help of Aristotle (Harmonic), with a link to type-check it online; the post reports that the work exposed a mistake in the formal-conjectures statement of the problem, for which van Doorn opened an issue. The file, in van Doorn's Lean-files repository (added 2026-03-02, linked above at the revision the formal-conjectures project pins), states Lean v4.24.0 and its Mathlib commit in its header, proves main_theorem (two sets of positive integers, each with at least $\tfrac14 \sqrt N$ elements up to $N$ for all large $N$, with no equal nonzero differences) and derives erdos_331, the negation of the statement that for all $A, B \subseteq \mathbb N$ with $N^{1/2} = O(\lvert A \cap [0, N) \rvert)$ and likewise for $B$, the set of quadruples $a_1 \neq a_2$ in $A$, $b_1, b_2$ in $B$ with $a_1 + b_2 = a_2 + b_1$ is infinite; the corrected formal-conjectures statement file (linked above at its revision of 30 September 2026), whose own theorem is sorry, states the same proposition and records the file as its formal proof. Boris Alexeev's repository lean-proofs carries a copy of the file for four Mathlib versions (linked above at its commit of 2026-09-15, with the repository's record page), whose header names Ruzsa as the informal author and Aristotle and Wouter van Doorn as the formal authors. The file declares itself a formalization of Ruzsa's counterexample, so it and its copies are listed on this page and have no page of their own. No formalized evidence is listed: that evidence means Lean this corpus built and audited, and the file is a third-party development. The disproof rests on the counterexample as the site records it and as Erdős and Freud published it.