Problem 948

Is there a function $f(n)$ and a $k$ such that in any $k$ -colouring of the integers there exists a sequence $a_1<\cdots$ such that $a_n<f(n)$ for infinitely many $n$ and the set

\left\{ \sum_{i\in S}a_i : \textrm{finite }S\right\}

does not contain all colours?

Source: erdosproblems.com/948

Number theory
Ramsey theory

Wiki page

Status

SolvedDisproved

An accepted solution exists. The statement is false.

Disproved; the site labels the problem SOLVED. The status-defining source is an AI-generated disproof, a note titled "A Negative Answer to an Erdős--Galvin Problem" (as its Lean formalization names it), produced by GPT Pro at the prompting of a contributor, Liam Price, who posted it to the site's thread on 21 June 2026 together with a Lean formalization made with Aristotle; the site's commentary credits the answer to GPT Pro, prompted by Price (the Lean file's header writes the model's name as GPT-5.5 Pro). The theorem: for every $f:\mathbb{N}\to\mathbb{N}$ there is a coloring of $\mathbb{N}$ by $\mathbb{N}$ such that for every strictly increasing sequence with $a_n<f(n)$ for infinitely many $n$ the finite sums take every color, hence for every $k$ a $k$ -coloring with the same property. Acceptance evidence: a review by Stijn Cambie, a contributor to the thread, whose comment of 22 June 2026 reports that it confirmed the proof; a screening comment of 21 June 2026; the adoption by the site's curator, Thomas Bloom (label SOLVED, page last edited 5 July 2026, the commentary's paragraph and the curator's sketch of the construction in the thread on 6 July 2026); the community database (6 July 2026) and the community's AI-contributions wiki (a full solution with a Lean formalization, 21 June 2026). This is a source-supported solution accepted by the site, distinct from a claim of journal refereeing: no refereed publication, no arXiv version and no written expert review beyond the thread were found on 2026-09-18. The argument document is an online editable document whose read link gives the editor's application page, with no PDF or export; the page rests on the site's account, the review comment and the Lean file [Le26], whose theorem statements and declared axioms are the basis here (this corpus has not built or audited it). Two vocabulary points about the label are recorded below. The claim page the 2026 coloring records the result, its postings and its acceptance evidence under the site's label, and the frontmatter standing derives from it; beside it, Galvin's two-coloring (Theorem 4.1 of [ErGa91], refereed and credited by the site's curator) is an accepted partial claim for the case $k=2$ .

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, p. 57. Library home: Erdos 1977.
ErGa91: Erdős, P. and Galvin, F., Some Ramsey-type theorems. Discrete Math. 87 (1991), no. 3, 261--269, doi:10.1016/0012-365X(91)90135-O (received 3 January 1989; February 1991 per the Crossref record; zbMATH 0759.05095). The PDF pages cited here are those of the publisher's open-archive file. The site cites p. 268 (PDF p. 8), which carries Theorem 4.1 (Galvin's coloring with its proof), Problem 4.2 (this problem) and Theorem 4.3 (the interval-sums theorem); Theorem 2.1 (p. 262, PDF p. 2) is quoted below. Library home: Erdős and Galvin 1991.
Pr26: "A Negative Answer to an Erdős--Galvin Problem", the argument note, title as given in the Lean file's docstring. Linked from the thread comment of 21 June 2026 as an online editable document (https://www.overleaf.com/read/grttvnmptzwz) and from the site's commentary as a project link (https://www.overleaf.com/project/6a37c43804fb818b104241f5). The read link returns the editor's application page (a script-driven page with a login form, no PDF and no export), so the document is inaccessible; the project link requires an account. Authorship as the thread and the site give it: prompted and posted by the contributor Liam Price, the argument credited to GPT Pro; the Lean file's header names the model GPT-5.5 Pro and prints the contributor's first name differently.
Le26: The Lean formalization: plby/lean-proofs src/latest/ErdosProblems/Erdos948.lean, the main head of 15 September 2026 (23,716 bytes; toolchain comment "leanprover/lean4:v4.33.0 mathlib v4.33.0"), not built by this corpus. The thread's comment of 21 June 2026 also links a Lean web-editor page whose URL embeds an earlier 369-line version of the same development, made with Aristotle (namespace ErdosGalvin, theorems main and main_finite; not built by this corpus).
FL20: Fernández-Bretón, D. and Lee, S. H., Hindman-like theorems with uncountably many colours and finite monochromatic sets. Proc. Amer. Math. Soc. 148 (2020), no. 7, 3099--3112, doi:10.1090/proc/14649; arXiv:1801.09179. Context for Erdős's variant with continuum many almost disjoint classes; its abstract is the basis here.

Problem 948

Status

Proof claims

Discussion