Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. Let be coprime and call representable if it is a sum of integers no one of which divides another. For each of the pairs , and there is an infinite sequence of non-representable numbers greater than whose terms are pairwise coprime and each coprime to ; in particular there are infinitely many non-representable coprime to , and infinitely many pairwise coprime ones, the two readings of the second question of Problem 1110. These are exactly the pairs that Yu and Chen [YuCh22] left open when they proved that there are infinitely many coprime non-representable numbers for , for with , and for with , so together with their theorem the second question is answered yes for every coprime pair other than . The claimant, the forum user Apiros3, posted the claim on the site's proof-claims tab on 2026-08-05 as a partial proof; the claim's tab names the AI systems GPT-5.6 Sol and GPT-5.5 as the tools that took part in writing the formalization, and the repository's own statement says the formalization was generated with OpenAI models and that its owner accepts responsibility for errors without claiming credit for model-generated work.
Submission note. Posted to erdosproblems.com as a proof claim by Apiros3 (account apiros3) on 5 August 2026, giving "GPT-5.6 Sol, GPT-5.5" as the AI used:
GPT-5.6 Sol and GPT-5.5 were used in the proof formalization. There are infinitely many coprime non-representable numbers. Yu and Chen reduced this problem to three cases (p,q) = (5,2), (9,2), (5,3), and we give a proof for these three. The proof is by picking a small seed c < p and then repeatedly forming larger coprime non-representable numbers of the form p^a + c q^M. The proof sketch is as follows: - Any representation is just a finite antichain of grid points (as no terms divide each other) - If an antichain sum in the rectangle 0 <= i <= a, 0 <= j < M is congruent to p^a mod q^M, then it is exactly p^a. - If N = p^a + c q^M has a representation, then c q^M < (p-1)p^a forces (a,0) to be a grid point. Removing this and dividing by q^M implies c is representable, a contradiction. The cases are each proven by seeds: - (5,2): c = 3 - (9,2): c = 5 - (5,3): c = 2
The argument. A representation is a finite antichain of lattice points in the divisibility order, with the summands. Fix a seed that is itself non-representable and coprime to , and consider for large and . If an antichain sum over the rectangle , is congruent to modulo , it equals . Because , a representation of must use the point ; removing it and dividing by would represent , a contradiction. The seeds are for , for and for . Each such is prime to by itself, since and with ; the recursive choice of the exponents and for each new term is what makes the terms of the sequence pairwise coprime. A comment in the thread of 2026-10-02 observes that the same seed device extends to every coprime pair other than and , with the smallest prime not dividing when is even and for the least prime factor of when is odd; that remark is a thread comment, not part of the claim.
Covers. The second question of the problem, infinitely many coprime non-representable numbers, in the pairwise-coprime reading and hence in the coprime-to- reading, for the three pairs , and , and through Yu and Chen's theorem, which the Lean development also proves, for every coprime pair with . The first question, the density of the non-representable numbers, is not addressed.
Formalization. The repository Apiros3/erdos1110 (Apache License 2.0,
Lean toolchain v4.32.1; the pinned commit of 2026-10-02 is the repository's
only commit) defines Erdos1110Conclusion p q as the existence of a sequence
of non-representable numbers greater than , each coprime to and
pairwise coprime, and declares the theorems
Erdos1110.exceptional_5_2_unconditional,
Erdos1110.exceptional_9_2_unconditional,
Erdos1110.exceptional_5_3_unconditional and their conjunction
Erdos1110.exceptional_cases_unconditional, which its README calls the new
contribution. It also proves Yu and Chen's range in Lean, unconditionally:
yuChenRange_unconditional discharges the pairs with , with and
, and with and through counting bounds that give the
representable numbers density zero (the representableDensityZero theorems
of Density/YuChen.lean), and the pairs and through
explicit constructions; erdos1110_unconditional and
Erdos1110.erdos1110_unordered assemble these with the three exceptional
pairs into the conclusion for every coprime pair of bases at least other
than , with no hypothesis beyond coprimality, and
erdos1110_setConclusion_unordered and
erdos1110_valueSetConclusion_unordered restate it as an infinite pairwise
coprime set, the form of the formal-conjectures statement. The forum claim's
write-up link, a Markdown file under docs/, is not in that commit, and the
README describes the manuscript as in preparation, so the repository is the
only retained posting. This corpus has not built or audited the development;
it is a formalization link and not formalized evidence.
Standing. Claimed. The site labels the problem open (page last edited 1 April 2026) and marks proof claims as unexamined by anyone associated with it. No review, publication or build is recorded here, and nothing on this page is independently reviewed by this project.