---

Claim. For the pair $(p,q)=(7,2)$ the representable integers, the sums of numbers $2^a7^b$ no one of which divides another, have positive lower density:

$$\liminf_{x\to\infty}\frac{1}{x}\,\#\{n\leq x: n\text{ representable}\}>0.$$

Yu and Chen's density-zero theorem [YuCh22] needs $p>10$ when $q=2$, so $(7,2)$ is outside it. The claimant, Jean-Roch Bécart, posted the claim on the site's proof-claims tab on 2026-09-29 as a partial proof, with the AI system named on the tab as Opus 5.5; the repository's draft of the same date, Integers representable by $\{7,2\}$-antichains have positive lower density, states that the proof, the programs and the Lean code were produced by Claude Opus 5.5 under the author's direction and have not been reviewed by a human expert. The method extends the finite-certificate approach of Ding, Li, Liu and Zhang for $(5,2)$. The pinned revision also holds a draft of the same date, Integers representable by $\{4,3\}$-antichains have positive lower density, with the same authorship statement, which states the same conclusion for $(p,q)=(4,3)$, another pair outside Yu and Chen's range (which needs $p>6$ when $q=3$); it was added to the repository later the same day, after the forum claim, is not posted on the forum, and is recorded here as the same claimant's same-day result.

Submission note. Posted to erdosproblems.com as a proof claim by Jean-Roch Bécart (account jbecart) on 29 September 2026, giving "Opus 5.5" as the AI used:

We show that for (p,q) = (7,2) the representable integers have positive lower density. This pair is not covered by Yu and Chen's density-zero result, which requires p > 10 when q = 2. Method. We extend the finite-certificate approach of Ding, Li, Liu and Zhang for (2,5). 1. Encoding. A residue $y$ mod $2^{sN}$ is encoded block by block, with $s = 11$ bits per block. Each block gets a chain $\{(\alpha,\gamma)\}$, strictly increasing in both coordinates, with $\sum 2^{\alpha}7^{-\gamma} \equiv$ (current block) mod $2^{s}$. 2. Antichain. The blocks are stacked so that the terms $2^{st+\alpha}\,7^{A-G_t-\gamma}$ form a divisibility antichain. The resulting integer satisfies $n \equiv 7^{A}y \pmod{2^{sN}}$, so the map $y \mapsto n$ is injective. 3. Look-ahead certificate. The chain chosen for each block depends on the next two blocks. A potential function $V$ on the $2^{22}$ states gives an average height increment of $\hat g = 3.904698\ldots$ per block. This is below $11\cdo Notes: Computer-assisted. The finite certificate (the table $V$ and the drift inequality over $2^{22}$ states) is checked by two independently written C programs. Both give the exact integer bound $\hat g\cdot 2^{31} = 8385274094$. We also check that $7^{26} < 2^{73}$. The reduction "certificate ⇒ positive lower density" is formalized in Lean 4 / Mathlib. It uses the formal-conjectures definition of Representable verbatim. It has no sorry and depends only on the standard axioms. Only the certificate check itself is trusted to the C code. The implied density constant is astronomically small. Numerically, about 22% of the integers up to $2^{27}$ are representable. The same method does not reach (9,2) or (5,3) at feasible sizes. The proof, programs and Lean code were produced by the AI under my direction. They have not yet been reviewed by a human expert, and feedback is welcome.

The argument. The construction reads a residue $y$ modulo $2^{sN}$ in $N$ blocks of $s=11$ bits. Each block is assigned a chain of exponent pairs $(\alpha,\gamma)$, increasing in both coordinates, whose terms $2^\alpha7^{-\gamma}$ add up to that block's value modulo $2^s$. Shifting the $t$-th block's terms to $2^{st+\alpha}7^{A-G_t-\gamma}$ makes all the terms pairwise non-dividing, and their sum $n$ is congruent to $7^Ay$ modulo $2^{sN}$, so distinct residues give distinct representable integers. Each block's chain is chosen with the two following blocks in view, and a potential function on the $2^{22}$ possible states certifies that the height grows by about $3.9047$ per block on average, below the threshold that keeps the constructed integers within a window of size comparable to $2^{sN}$; that is the positive proportion. The certificate, a table and a drift inequality over the $2^{22}$ states, is checked by two independently written C programs, both returning the exact integer bound $8385274094$ for the increment times $2^{31}$; the inequality $7^{26}<2^{73}$ is checked as well. The implied density constant is very small, while a computation reports that about $22\%$ of the integers up to $2^{27}$ are representable. The author states that the method does not reach $(9,2)$ or $(5,3)$ at feasible sizes. For $(4,3)$ the draft notes congruence obstructions (no representable $n$ is $2$ modulo $3$ or $2$ modulo $4$) that recur at every scale, so the method is extended with a viable set of states: blocks of two base-$4$ digits, states of $14$ digits ($2^{28}$ of them), of which two thirds are viable, and a potential found by value iteration; the drift inequality is checked exactly by a C program over all viable states and spot-checked by a Python program.

Covers. The first question of Problem 1110, the density of the non-representable numbers, for the two pairs $(7,2)$ and $(4,3)$: the representable integers have positive lower density, so the non-representable ones do not have density one. Nothing is claimed about natural density, other pairs, or the second question. The claim value is proved: the result proves a lower bound for these pairs, positive lower density of the representable integers, without determining the density.

Formalization. The file lean/E1110.lean (1112 lines; Lean v4.32.0-rc1 and the Mathlib revision the repository's README records) proves E1110.pos_lower_density: from a certificate K : Cert s H with drift K.g below a parameter $\lambda$ satisfying $7^\lambda<2^s$, the set of representable integers has positive lower density, with Representable taken verbatim from the formal-conjectures statement of the problem. The specialization E1110.erdos1110_72_density takes $s=11$, $H=10$ and the hypothesis that a certificate with K.g = 8385274094 / 2^31 exists, which is the fact the C programs check and the only part outside Lean. The author reports no sorry or native_decide and the axioms propext, Classical.choice and Quot.sound. For $(4,3)$ the file 4-3/lean/E1110G.lean at the same revision proves the reduction for general coprime bases as E1110G.pos_lower_density, specialized in E1110G.erdos1110_43_density to the existence of the checked certificate, which the draft reports as free of sorry and using standard axioms only. This corpus has not built or audited either development or rerun the C checkers; the files are formalization links and not formalized evidence.

Standing. Claimed. The site labels the problem open (page last edited 1 April 2026), the author describes the proof as unreviewed by a human expert, and no review or publication is recorded. Nothing on this page is independently reviewed by this project.