Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated


Claim. Let p>q≥2p>q\geq 2 be coprime and call nn representable if it is a sum of integers pkqlp^kq^l no one of which divides another. For each of the pairs (p,q)=(5,2)(p,q)=(5,2), (9,2)(9,2) and (5,3)(5,3) there is an infinite sequence of non-representable numbers greater than 11 whose terms are pairwise coprime and each coprime to pqpq; in particular there are infinitely many non-representable nn coprime to pqpq, 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 q>3q>3, for q=3q=3 with p≠5p\neq 5, and for q=2q=2 with p∉{3,5,9}p\notin\{3,5,9\}, so together with their theorem the second question is answered yes for every coprime pair other than {2,3}\{2,3\}. 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 (i,j)(i,j) in the divisibility order, with piqjp^iq^j the summands. Fix a seed c<pc<p that is itself non-representable and coprime to pqpq, and consider N=pa+cqMN=p^a+cq^M for large aa and MM. If an antichain sum over the rectangle 0≤i≤a0\leq i\leq a, 0≤j<M0\leq j<M is congruent to pap^a modulo qMq^M, it equals pap^a. Because cqM<(p−1)pacq^M<(p-1)p^a, a representation of NN must use the point (a,0)(a,0); removing it and dividing by qMq^M would represent cc, a contradiction. The seeds are c=3c=3 for (5,2)(5,2), c=5c=5 for (9,2)(9,2) and c=2c=2 for (5,3)(5,3). Each such NN is prime to pqpq by itself, since N≡cqM(modp)N\equiv cq^M\pmod p and N≡pa(modq)N\equiv p^a\pmod q with gcd⁡(c,p)=1\gcd(c,p)=1; the recursive choice of the exponents aa and MM 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 (4,3)(4,3) and (6,5)(6,5), with cc the smallest prime not dividing pqpq when pqpq is even and c=t−1c=t-1 for tt the least prime factor of pqpq when pqpq 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-pqpq reading, for the three pairs (5,2)(5,2), (9,2)(9,2) and (5,3)(5,3), and through Yu and Chen's theorem, which the Lean development also proves, for every coprime pair p>q≥2p>q\geq 2 with {p,q}≠{2,3}\{p,q\}\neq\{2,3\}. 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 11, each coprime to pqpq 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 q>3q>3, with q=3q=3 and p>6p>6, and with q=2q=2 and p>10p>10 through counting bounds that give the representable numbers density zero (the representableDensityZero theorems of Density/YuChen.lean), and the pairs (4,3)(4,3) and (7,2)(7,2) 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 22 other than {2,3}\{2,3\}, 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.