---

Claim. For every three pairwise coprime integers $a,b,c>1$, every sufficiently large integer is a sum of distinct integers of the form $a^kb^lc^m$ ($k,l,m\geq 0$) no one of which divides another. This answers the question of Problem 123 in the affirmative: the sequence $\{a^kb^lc^m\}$ is $d$-complete in the sense of Erdős and Lewin, whose paper [[../library/diophantine_problems/erdos_1996_d_complete_sequences_integers/_index|$d$-complete sequences of integers]] posed the conjecture.

The claimant is Colin Snyder (forum name coffeewithcolin), who posted the result on the site's proof-claims page on 2026-07-15 through Star Fleet Math. The claim's entry names the system that found the proof as GPT 5.6 in a custom harness. The written forms are the solution page and a Lean 4 development distributed as a verification bundle; the claimant reports the theorem Erdos123.erdos_123, built against Mathlib, whose axioms are propext, Classical.choice and Quot.sound with no sorry. The claimant's note records that the reading $a,b,c\geq 1$ fails at $(1,1,1)$ and that the bundle proves the reading $a,b,c>1$, which is the site's statement and the encoding of the formal-conjectures file.

Submission note. Posted to erdosproblems.com as a proof claim by Colin Snyder (account coffeewithcolin) on 15 July 2026, giving "GPT 5.6 (custom harness)" as the AI used, which the site marks as accepted as correct:

We claim the answer is yes for all pairwise coprime $a,b,c>1$: every large integer is a sum of distinct terms $a^ib^jc^k$, none dividing another. Proved in Lean 4 / Mathlib (theorem Erdos123.erdos_123), standard axioms only, no sorry. Idea: on a fixed homogeneous level $i+j+k=D$, coprimality makes divisibility coordinatewise, so no term on the level divides another and the problem becomes purely additive. Van der Waerden (via Hales-Jewett) gives long arithmetic progressions of representable sums, which act as radix digits to build a represented interval. Unused terms on the same level are smaller than the interval width, so adding them optionally stretches the interval without raising its floor. One wide interval plus the Erdős-Lewin residue reduction gives completeness. Notes: The literal $a,b,c\ge 1$ fails at $(1,1,1)$; the bundle records that counterexample and proves the intended $a,b,c>1$ reading (matching the Formal Conjectures encoding). Verify: "lake exe cache get && lake build", then "#print axioms Erdos123.erdos_123" gives exactly [propext, Classical.choice, Quot.sound].

Argument, in outline. As the claimant describes it, the proof works with the terms whose exponents share one total $i+j+k=D$. Because the bases are pairwise coprime, one such term divides another only when each exponent of the first is at most the corresponding exponent of the second, which never happens within a single total, so the divisibility condition drops out and only an additive question remains. Van der Waerden's theorem, obtained through Hales–Jewett, supplies long progressions of sums that are representable; these play the role of digits in a positional system, and the system fills a whole interval of integers. Terms of the same total that the construction has not spent are smaller than that interval is wide, so including or omitting them widens the interval while its lower end stays fixed. A single interval wide enough, combined with the reduction modulo residues of Erdős and Lewin, yields completeness. This page records the claimant's outline only; the argument has not been reconstructed in this corpus.

Acceptance. The site's curator, Thomas Bloom, marks the problem PROVED (LEAN), records this proof claim as accepted by the site as correct, and credits the resolution to GPT 5.6 with Snyder as its prompter (problem page last edited 17 July 2026): that curator acceptance is the reviewed evidence. There is no refereed publication. The solution page reports that an independent referee rebuilt the Lean project and audited the compiled definitions against the statement; that report is the claimant's own and is not outside review. The Lean development was not built or audited by this corpus, so the page lists no formalized evidence; the Lean qualification in the site's label refers to the claimant's development.

Copies of the formalization. Boris Alexeev's repository holds a copy of the development at the commit linked above; its header calls itself a formalization of a solution to the problem and lists as authors Star Fleet Math, Claude Fable 5, Colin Snyder and the Formal Conjectures authors. That author list names a different system from the claim's entry; both attributions are recorded here as the sources give them and neither is resolved. The formal-conjectures statement file, at its commit of 2026-09-18, marks erdos_123 solved and names that copy, at the same commit as the link above, as its formal proof. A later, independent proof by Principia Math has its own page, Principia Math's proof.