← Star Fleet Math

Erdős Problem #123

Erdős Problem

www.erdosproblems.com/123

The problem

Let a,b,c≥1a,b,c\geq 1 be three integers which are pairwise coprime. Is every large integer the sum of distinct integers of the form akblcma^kb^lc^m (k,l,m≥0k,l,m\geq 0), none of which divide any other?

(Erdős Problem #123 — prize: $250 — number theory — https://www.erdosproblems.com/123)

Result

For every pairwise-coprime triple of integers a,b,c>1, every sufficiently large integer is a sum of distinct terms a^i b^j c^k such that no selected term divides another. In Lean, this is the theorem Erdos123.erdos_123 : Erdos123.IntendedStatement.

def IntendedStatement : Prop :=
  ∀ a b c : ℕ, 1 < a → 1 < b → 1 < c → PairwiseCoprime3 a b c →
    IsDComplete (Smooth3 a b c)

/-- Erdős Problem 123 for the intended nondegenerate hypothesis `a,b,c>1`. -/
theorem erdos_123 : IntendedStatement := intended_erdos_123

Independent referee

The agent claims a complete Lean 4 + Mathlib proof (Erdos123.erdos_123) of Erdős Problem #123 in its intended nondegenerate form: for all pairwise-coprime a,b,c > 1, the set {a^k b^l c^m} is d-complete (every sufficiently large integer is a sum of distinct such terms, none dividing another). I independently rebuilt the full pinned project (Lean v4.31.0, Mathlib fabf563a7c) from the attached sources — which are byte-identical to the redundant tarball — and reproduced everything myself: lake build exited 0 with 8596 jobs, a ripgrep scan found no sorry/admit/axiom/native_decide/unsafe/macro/notation/instance tricks anywhere in Research/, and #print axioms reports exactly [propext, Classical.choice, Quot.sound] with no sorryAx. I printed the compiled definitions from the built environment and audited them quantifier-for-quantifier against problem.md: Smooth3, Finset-distinctness, the divisibility antichain (IsPrimitive), and the ∃N ∀n≥N threshold are all faithful, and the statement matches the independent Google DeepMind Formal Conjectures encoding of #123 (which is tagged 'research open' and itself uses a,b,c > 1, noting >1 is required to avoid degenerate reduction). One transparent caveat for human review: problem.md literally writes a,b,c ≥ 1, which is formally false at (1,1,1) — the project proves that refutation too (not_literalStatement) — so the theorem proved is the >1 source conjecture, exactly as the Formal Conjectures encoding pins it; the excluded degenerate case a=1 (two-base reduction) is not covered by this theorem.

Report

Solving Erdős Problem 123

The problem and why it resisted the usual induction

For pairwise-coprime integers a,b,c>1a,b,c>1, consider the numbers

aibjck(i,j,k≥0). a^i b^j c^k \qquad (i,j,k\ge 0).

The question asks whether every sufficiently large integer is a sum of distinct such numbers, with the additional requirement that no chosen summand divides another.

The divisibility condition is the real source of difficulty. Ordinary completeness arguments can use many terms from different scales, but terms from different scales tend to be comparable by divisibility. Conversely, a set chosen to be a divisibility antichain can be too arithmetically sparse to fill consecutive integers.

Earlier work had developed a powerful reduction scheme: choose a correction with the required residue modulo one base, subtract it, divide by that base, and induct. For particular triples this succeeds after a finite computer check. In general, however, it leaves a stubborn finite-seed problem: one must first represent every integer in a multiplicatively wide interval [N,CN][N,CN]. The correction induction does not construct that interval; it only propagates it.

This explains why several attractive partial ideas did not finish the problem:

  • A signed identity of difference one gives two consecutive sums, but one residue representative per class necessarily has spread at least the modulus minus one. A width-one interval cannot grow under ordinary residue gluing.
  • Complete residue systems on a primitive level solve congruences, but say nothing about their numerical spread.
  • Van der Waerden and Hales–Jewett arguments produce arbitrarily long arithmetic progressions of primitive sums, but initially with an uncontrolled common difference.
  • Even after fixing the common difference, a progression B0+rdB_0+r d carries a large positive baseline B0B_0. Replicating such progressions increases width and baseline at the same rate, so it need not produce the multiplicatively wide seed required by induction.

The important lesson was that large additive width is not enough. The lower endpoint has to remain under quantitative control.

The homogeneous-level coordinate system

The first structural simplification is to work on one homogeneous exponent level

i+j+k=D. i+j+k=D.

For pairwise-coprime bases greater than one, divisibility of monomials is coordinatewise comparison of their exponents. Therefore two distinct monomials on the same level can never divide one another. Every subset of a homogeneous level is automatically primitive.

This turns the problem into an additive question about subset sums while making primitiveness essentially free—as long as all pieces of the construction can be placed on the same exact degree.

An edge-code construction supplies cnc^n primitive subset sums on one level with distinct residues modulo cnc^n and a bounded carry. Coloring by that carry and applying finite van der Waerden, itself obtained from Mathlib’s Hales–Jewett theorem, gives arbitrarily long exact arithmetic progressions of primitive homogeneous subset sums.

Turning one AP into a large lattice interval

Order the bases as

1<a<c<b. 1<a<c<b.

Choose

H=edgeDigitDepth⁡(c),u=H+2, H=\operatorname{edgeDigitDepth}(c),\qquad u=H+2,

and then choose v>0v>0 so that

2bav≤cv. 2b a^v\le c^v.

Define two coprime homogeneous translation weights

A=au+v,B=bucv. A=a^{u+v},\qquad B=b^u c^v.

Copies of one AP digit family are translated by the weights

AM−rBr. A^{M-r}B^r.

The choice u>H+1u>H+1 places different copies in disjoint bands of the bb-exponent. Multiplying every term by abcabc makes every AP term strict-interior. All copies then lie on one exact exponent degree.

A bounded homogeneous-radix lemma proves that coefficient sums

∑r=0MsrAM−rBr,0≤sr<4AB, \sum_{r=0}^{M} s_r A^{M-r}B^r, \qquad 0\le s_r<4AB,

contain a full interval of width at least 2ABM+12AB^{M+1}. Replacing each coefficient by the corresponding AP digit set realizes this as an interval on a lattice of step abc dabc\,d, where dd is the AP difference.

Filling residues with face corrections

The next ingredient constructs, on every sufficiently high exact degree, a primitive correction for each residue modulo any prescribed modulus. The corrections are supported on the three coordinate faces and, in the ordered case, have total size bounded by

CcorrcD. C_{\mathrm{corr}}c^D.

Apply this with modulus abc dabc\,d, on the same exact degree as the AP-radix construction. Face-supported corrections are disjoint from the strict-interior AP terms. Moreover,

Bcu+v=(bc)u>1, \frac{B}{c^{u+v}}=\left(\frac bc\right)^u>1,

so exponential domination gives

CcorrcD=o(BM). C_{\mathrm{corr}}c^D=o(B^M).

Thus the correction spread is eventually smaller than the radix width. Residue gluing converts the lattice interval into an ordinary consecutive interval [LM,UM][L_M,U_M] satisfying

abc BM≤UM−LM,LM≤KBM+1 abc\,B^M\le U_M-L_M, \qquad L_M\le K B^{M+1}

for a fixed constant KK.

At this stage there is a genuine interval, but its multiplicative width is still only bounded by a constant. This is exactly where the earlier baseline problem remained.

The key breakthrough: an optional interior shell

The decisive idea was to exploit monomials that had not yet been used, on the same exact homogeneous level.

For each of linearly many indices ss, fix a bb-exponent just beyond every AP band. Among the remaining a,ca,c-exponents, choose the last point of the geometric grid

bsaR−kck b^s a^{R-k}c^k

below a target of size cvMc^{vM}. Because consecutive grid points differ by the fixed factor c/ac/a, the selected monomial lies in a controlled multiplicative window. After restoring the common factors, this produces at least M−O(1)M-O(1) distinct optional monomials zz satisfying

z≤X,aX≤cz,X=abc BM. z\le X, \qquad aX\le cz, \qquad X=abc\,B^M.

Every optional term is therefore no larger than the already available interval width. Adding such a term optionally—either use it or do not—extends a consecutive interval without changing its lower endpoint. Since all optional terms remain on the same exact level and lie beyond the AP exponent bands, primitiveness and disjointness are preserved.

Their combined contribution is

Ω(MBM), \Omega(MB^M),

while the lower endpoint remains O(BM)O(B^M). Hence the ratio of the upper endpoint to the lower endpoint grows linearly with MM. For every requested R>1R>1, and beyond every requested lower threshold, this constructs a primitively represented interval

[N,RN]. [N,RN].

This interior-shell amplification is what removes the finite-seed obstruction. The successful coordinate change was not merely “work on a homogeneous level,” but “place the main growth along an interior homogeneous ray, then use the unused transverse strip as optional mass.”

Completing the induction

The residue-reduction argument was strengthened to a flexible finite-seed gate: there are constants N0N_0 and C>1C>1 such that any represented interval [N,CN][N,CN] with N≥N0N\ge N_0 implies d-completeness.

Applying the arbitrary-width construction with R=CR=C proves d-completeness for ordered bases 1<a<c<b1<a<c<b. Pairwise-coprime bases greater than one are distinct, so every triple has one of six strict orderings. Explicit permutations of the exponents show that permuting the bases leaves the smooth set unchanged, completing all cases.

Verification

The proof is formalized in Lean 4 with Mathlib. The final theorem is

Erdos123.erdos_123 : Erdos123.IntendedStatement

where IntendedStatement quantifies over all pairwise-coprime natural bases greater than one and asserts an explicit eventual threshold for primitive representations.

The complete project builds successfully, and a source scan finds no proof placeholders. Lean’s axiom report for the final theorem is exactly

[propext, Classical.choice, Quot.sound]

with no sorryAx. The webpage literally writes a,b,c≥1a,b,c\ge1; that universal formulation is false at (1,1,1)(1,1,1). The project records this separately and proves the intended nondegenerate a,b,c>1a,b,c>1 conjecture used in the source literature and independent formal-conjecture encoding.

Download Full Solution & Verify with Your AI

The download contains everything needed to verify this solution independently: the original problem, the formal statement, the complete pinned Lean project, and the verifier script — plus step-by-step instructions for your agent. About 20 minutes, mostly downloading Mathlib.

↓ Download full solution raw