---

Claim. For every $f:\mathbb{N}\to\mathbb{N}$ there is a coloring $\chi_f:\mathbb{N}\to\mathbb{N}$ with countably many colors such that, for every strictly increasing sequence $a_1<a_2<\cdots$ with $a_n<f(n)$ for infinitely many $n$, the finite sums $\sum_{i\in S}a_i$ over nonempty finite $S$ take every color; reducing the color modulo $k$ gives, for every $k\ge2$, a $k$-coloring with the same property. So no function $f$ and no number $k$ of colors have the property that Problem 948 asks for, and the answer is no, for finitely many colors and for $\aleph_0$ colors alike. A sequence with $a_n<f(n)$ for all $n$ has it for infinitely many $n$, so the same coloring answers the "all $n$" reading of Erdős's printed question. The claimant is Liam Price, who prompted GPT Pro for the argument and posted it to the site's thread on 21 June 2026 as a note titled "A Negative Answer to an Erdős--Galvin Problem" (the title the Lean file's docstring gives), together with a Lean formalization made with Aristotle; the site's commentary credits the answer to GPT Pro, prompted by Price. The site labels the problem SOLVED, its label for a resolution that is neither a proof nor a disproof, although the answer is negative; the claim value here records the mathematical outcome, a disproof, and the site's label is recorded in the problem page's Status.

The construction (as the site's curator sketched it in the thread on 6 July 2026 and as the Lean file defines it; the note itself is inaccessible). With $G$ a fast-growing function chosen from $f$, the color of $n$ is one less than the number of intervals of the shape $[k,G(k)]$ that a greedy procedure needs to cover the positions of the nonzero binary digits of $n$. For a sequence with $a_n<f(n)$ infinitely often, take $n$ with $a_n<f(n)$ and $2^k<n\le2^{k+1}$: two of the $n+1$ initial sums of $a_1,\ldots,a_n$ are congruent modulo $2^k$, so their difference, a block of consecutive terms, has sum divisible by $2^k$ and at most $nf(n)\le2^{G(k)}$, so its binary digits lie in one interval of the shape above and the block sum has the first color; repeating this on disjoint index intervals whose digit blocks are separated produces a sum of every color. The screening comment describes the argument as similar to Erdős and Galvin's 1991 paper and an extension of it; that paper's Theorem 4.1 is Galvin's two-color example, recorded on its own claim page.

Acceptance. Reviewed: Stijn Cambie (the thread account StijnC), a contributor to the site's thread independent of the claimant, reviewed the argument and reported in a comment of 22 June 2026 that Cambie's review had confirmed the proof, with minor comments sent to the author for the note; the site marked the comment as addressed. The site's curator, Thomas Bloom, then adopted the answer: label SOLVED, page last edited 5 July 2026, the commentary's credit of the answer to GPT Pro prompted by Price, and the curator's own sketch of the construction in the thread on 6 July 2026. The community database lists the problem as solved as of its last update on 6 July 2026, and the community's AI-contributions wiki lists the contribution of 21 June 2026 as a full solution with a Lean formalization. A screening comment of 21 June 2026 reports a screening check, linked from the comment, that found no issue and judged the Lean to match the paper. Not refereed: no written expert review beyond the thread was found. Not formalized in this schema's sense: the Lean artifact below was neither built nor kernel-checked in this corpus, and no statement-fidelity review exists, so formalized is not listed.

The Lean artifact. The thread's comment of 21 June 2026 links a Lean web-editor page whose URL embeds a 369-line development (namespace ErdosGalvin, theorems main and main_finite), made with Aristotle; that URL is not listed above, because its fragment is the compressed code itself and the complete address is not recorded, so the thread comment is its posting. The same development, extended, is the file src/latest/ErdosProblems/Erdos948.lean of the GitHub repository plby/lean-proofs, added on 18 August 2026 and linked above at the main head of 2026-09-18 (committer date 15 September 2026; Lean and Mathlib v4.33.0). Its header names Price and GPT-5.5 Pro as the informal authors and Codex and GPT-5.6 Sol as the formal authors. Its theorem countable states that for every f : ℕ → ℕ there is χ : ℤ → ℕ such that every strictly monotone a : ℕ → ℤ with a n < f n for infinitely many n has, for every color c, a nonempty finite index set I with χ (∑ i ∈ I, a i) = c; finite, finite_int and finite_nat give the finite-color and natural-number forms, and erdos_948_nat and not_erdos_948 negate the packaged positive assertion. The formal-conjectures statement file for the problem, added on 18 September 2026 and described on the problem page, points its formal_proof attribute at finite (line 451 of this file at the linked commit); a statement file is not a formalization link and is not listed above. The file contains no sorry and no axiom declaration and ends with a #print axioms command whose output is not recorded. A point about its statements (no fidelity review exists): the packaged positive assertion quantifies over all finite index sets including the empty one, so its negation alone is slightly weaker than the negation of the site's statement with nonempty $S$; the theorems countable, finite and finite_nat, which produce a nonempty index set for every color, cover the site's reading directly.

Read depth. The argument note is inaccessible: its read link gives the editor's application page with no PDF or export, and its content is known from the site's sketch and the Lean file. No step of the argument has been checked in this corpus, and nothing in it is independently reviewed. An exported PDF or an arXiv version of the note would close that gap.