The team solved Erdős Problem #123 (prize: $250) using 20 Codex accounts in parallel, formalizing the proof in Lean. The problem asks whether every large integer is a sum of distinct terms a^i b^j c^k with pairwise-coprime a,b,c>1, where no term divides another.

Previous approaches failed because the divisibility condition created a finite-seed obstruction: induction could propagate representations but not construct the initial multiplicatively wide interval [N, CN]. The breakthrough came from working on a homogeneous exponent level i+j+k=D, where primitiveness is automatic.

Using an edge-code construction and finite van der Waerden (from Mathlib's Hales–Jewett theorem), they built arithmetic progressions of primitive subset sums. A homogeneous-radix lemma with translation weights A=a^{u+v}, B=b^u c^v produced a lattice interval. Face corrections handled residues modulo abc·d.

The decisive interior shell amplification used unused monomials on the same level. Optional terms z satisfying z≤X, aX≤cz (X=abc·B^M) extended the upper endpoint while keeping the lower endpoint fixed, achieving ratio growing linearly with M. This removed the finite-seed obstruction, proving every sufficiently large integer is primitively representable.