Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 949
claims/: The 1 claim page of Problem 949, one per claimant's result; the problem's standing derives from them.
Statement. Let be a set containing no solutions to . Must there be a set of cardinality continuum such that ?
Formulation. The site's wording (page last edited 11 January 2026). "No solutions to " with makes sum-free, included, so for ; the formal-conjectures statement encodes exactly this. includes the doubles . Erdős's 1977 wording (printed p. 57, quoted below) asks for a set "of power in the complement of so that all the sums also belong to the complement of "; it does not say whether is allowed, and this page follows the site's . The site's discussion records that its earlier wording asked instead for with (a set closed under addition), that an explicit sum-free (the union of the intervals , ) refutes that wording, and that the wording was corrected on 17 and 18 August 2025 to the present one, which that does not refute ( works for it). The site's commentary calls Sidon when the sums with are distinct apart from .
Status. Open. No proof or disproof of the statement for an arbitrary sum-free was found in the search whose scope the Current assessment records. Two special cases are not the problem. The case Sidon (the site's variant) is claimed by an argument that AlphaProof found, merged as a Lean proof into the formal-conjectures statement file on 6 January 2026, posted to the site's discussion on 7 January 2026 and adopted by the site's commentary; the first case of that argument also covers every of cardinality less than without the Sidon hypothesis. It is recorded as a pending partial claim on its claim page, which the commentary on an open problem does not make accepted. The case of with the property of Baire is argued in a thread comment of 23 January 2026, not adopted by the commentary; it is a thread post, not a dated manuscript or a Lean proof, so it has no claim page. The proof-claim tab is empty. This is a bounded negative finding, not a certificate of openness.
Source. erdosproblems.com/949, accessed 2026-09-18: the problem page (OPEN, with the site's note that no finite computation can settle it; last edited 11 January 2026; source key [Er77c]), its eight-comment discussion thread (17 August 2025 to 23 January 2026) and its empty proof-claim tab. Cite as: T. F. Bloom, Erdős Problem #949, https://www.erdosproblems.com/949, accessed 2026-09-18.
References.
- [Er77c] Erdős, P., Problems and results on combinatorial number theory. III. Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976), Lecture Notes in Math. 626, Springer (1977), 43--72; Section 6, printed p. 57 (p. 15 of the public scan https://users.renyi.hu/~p_erdos/1977-27.pdf). The library holds no copy. Library home: erdos_1977_problems_results_combinatorial_number_theory_iii.
Formalization. Statement, with a proved variant. The file
ErdosProblems/949.lean
of formal-conjectures, at the commit the link pins,
declares
erdos_949 : answer(sorry) ↔ ∀ S : Set ℝ, (∀ a ∈ S, ∀ b ∈ S, a + b ∉ S) → ∃ A ⊆ Sᶜ, #A = 𝔠 ∧ A + A ⊆ Sᶜ
under category research open, with proof sorry, and the variant
erdos_949.variants.sidon : answer(True) ↔ ∀ S : Set ℝ, IsSidon S → ∃ A ⊆ Sᶜ, #A = 𝔠 ∧ A + A ⊆ Sᶜ
under category research solved, proved inside the file (lines 44 to 113, no
sorry), a proof carried by the collection file itself and recorded on
its claim page.
The community database records the problem open, the
statement formalized, formal_status unformalized and no formal proof
(record last updated 31 August 2025); the site's indicator reports a
formalized statement. The corpus has not built the file.
Current assessment
The question (site formulation, accessed 2026-09-18). The statement above; OPEN, with the site's note that no finite computation can settle it, last edited 11 January 2026. The commentary records Erdős's suggestion that, should the answer be no, one could assume instead that is Sidon (all sums with distinct up to the order of the summands), and states that a comment in the thread (the account YaelDillies) proves this variant affirmatively, by an argument that AlphaProof found: every Sidon set admits of cardinality continuum with . The thread, oldest first: a comment of 17 August 2025 (the account DesmondWeisenberg) answering the then-current wording in the negative with (sum-free; every that is not a multiple of has a multiple in , so the subsets of closed under addition are sub-semigroups of , all countable), later edited to note that the corrected problem asks for , which the construction does not resolve; a comment of 17 August 2025 (the account Vjeko_Kovac) pointing out that the site's wording did not match the original paper (p. 57), giving the present wording and, for that , ; a reply of 18 August 2025 that the commenter has no counterexample to the corrected formulation; three comments of 18 and 24 August 2025 (Vjeko_Kovac and another commenter) on what a nontrivial would have to look like ( must contain points arbitrarily close to , else a small ball around serves as ); the comment of 7 January 2026 (YaelDillies) with the Sidon argument below, which AlphaProof found, and links to the Lean proof AlphaProof discovered and to a cleaned-up version of it, after which the site was updated; and a comment of 23 January 2026 (the account Przemek Chojecki) proving the statement when has the property of Baire, remarking that the first case of the Sidon argument already covers every with without the Sidon hypothesis, and concluding that a counterexample would have to be very pathological: not Sidon, not measurable and without the property of Baire. The proof-claim tab is empty.
The origin ([Er77c], printed p. 57). In Section 6, "Problems on infinite subsets", after the Graham--Rothschild conjecture proved by Hindman (Problem 532) and the question with Galvin's construction that is Problem 948, Erdős first asks, as a "second possibility" for the real line, whether for every partition of the reals into two classes there is a sequence with for infinitely many all of whose subset sums lie in one class, and then poses the present question: "Let [sic] be a set of real numbers so that the equation is not solvable in . Is there then a set of power in the complement of so that all the sums also belong to the complement of ?", adding that, should the answer be no, one might instead assume that all the sums with are distinct. The first "" is printed with a stray subscript , a misprint for the of the rest of the passage; the closing sentence is the Sidon suggestion of the site's commentary. The passage poses the question and records nothing about it.
The Sidon variant (adopted by the site's commentary, found by AlphaProof;
not the problem). The argument posted on 7 January 2026 and carried by the
collection's erdos_949.variants.sidon at the pinned commit:
if , Zorn's lemma gives a maximal with
; maximality means every outside , outside and
outside already lies in , so
, and since the left side
has cardinality while the right has cardinality at most
, is impossible. This case does not use the
Sidon hypothesis, which is the thread's remark that every of cardinality
below is covered. If , pick , ,
and set : the Sidon property gives
, so , and
is disjoint from . Two
elementary steps were checked here as an observation: if and
with then , so the Sidon property forces
(since would give ); and if with $x,y\in
S\setminus{a}$ then are two representations of one number as a
sum of two elements of , so the Sidon property forces ,
contradicting . The site's commentary adopts the result; the Lean
proof in the collection file has no sorry, and the corpus has not built it;
no refereed source exists. The thread credits the argument and the Lean proof
to AlphaProof and the cleaning-up to the commenter. The variant is not the
problem, and its claim page records it as a pending partial claim.
The Baire case (a discussion proof; a lead, not status). The comment of 23 January 2026: if contains a neighborhood of , take ; otherwise is in the closure of , and is then meagre (if were comeagre in an interval , a small would give with , contradicting sum-freeness), so the set of "bad pairs" is meagre in , and a theorem of Mycielski (cited by name in the comment, without a reference) gives a perfect set with disjoint from it; has cardinality . The argument is not reviewed in this corpus; the site's commentary does not mention it. Together with the Sidon case it leaves, as the comment says, only non-Sidon sets of size without the property of Baire (and, by the measurable analog the comment gestures at, non-measurable) as possible counterexamples.
Adjacent question. Problem 965 asks, for an arbitrary -coloring of , for a set of size whose sums of distinct pairs are monochromatic, and is answered negatively in ZFC; here the two classes are a sum-free and its complement, the sums are required to fall into the complement, and itself must lie there.
Search scope. None of the routes below found a proof or disproof of the statement for arbitrary sum-free , or a proof claim.
- The site: problem page, discussion thread and proof-claim tab; the formal-conjectures file at the pinned commit, including the variant's proof; the community database as of 2026-09-18.
- arXiv: the API queries
abs:"sum-free" AND abs:continuum(no records),abs:"sum-free" AND abs:"real numbers"(one record, on primitive sets, not this problem) andabs:"pairwise sums" AND (abs:uncountable OR abs:continuum OR abs:reals)(five records; the only relevant one is the Hindman--Leader--Strauss paper of Problem 965, which does not treat sum-free classes). The API searches titles and abstracts only, so its zeros are weak. - The primary source: [Er77c] printed p. 57, in the public scan the References cite.
Not searched: MathSciNet, zbMATH, Google Scholar, X. The account of the Sidon variant follows the formal-conjectures file at the linked commit; the claim page links the pull request that carries AlphaProof's own version. Not held: [Er77c], of which the library holds no copy; the Mycielski theorem invoked in the thread is not identified to a paper.
Remaining gaps. (1) Nothing proves or refutes the statement for an arbitrary sum-free ; there is nothing to compile. (2) The Sidon variant rests on an argument that AlphaProof found, adopted by the site's commentary and formalized inside the collection file; the corpus has not built the file, and the claim stays pending. (3) The Baire-case argument is a discussion proof, unreviewed and not adopted by the site. (4) The origin passage is quoted as printed; its "" is marked as a misprint.
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.