---

Claim. Let $a,b>1$ be coprime integers. Every sufficiently large integer is a sum of distinct integers of the form $a^kb^l$ with $k,l\geq 0$: the set $\{a^kb^l\}$ is complete. This is the statement of Problem 246, in its corrected Statement, which takes $a,b\geq2$, and it is the theorem of B. J. Birch, Note on a problem of Erdős, Proc. Cambridge Philos. Soc. 55 (1959), no. 4, 370--373. The paper is not held; its record gives the issue as October 1959 and no day, so the page is dated by the first of that month. Davenport observed in the same note that the exponent $l$ can be bounded in terms of $a$ and $b$; the quantitative forms of that observation are on the problem page.

Acceptance. The result appeared in a refereed journal in 1959, the refereed evidence. The site's curator, Thomas Bloom, marks the problem PROVED and credits Birch (problem page last edited 7 December 2025): that curator credit is the reviewed evidence. Cassels, in his 1960 paper, records Birch's result as an immediate consequence of his more general Theorem I, a second proof with its own page, Cassels's criterion. The theorem is now called the Erdős--Birch theorem; Fang and Chen's quantitative form states it as its Theorem A.

Formalization. The site's "(LEAN)" suffix refers to a Lean 4 development in Boris Alexeev's repository, announced on the site's thread on 2025-12-28 (post 2513) and named, on that repository's main branch rather than at a fixed commit, as the formal proof of erdos_246 by the formal-conjectures statement file at its commit of 2026-09-18. Its header declares itself a formalization of a solution to the problem and lists two author groups, informal authors Birch and ChatGPT and formal authors Aristotle and Alexeev; in the thread post Alexeev writes that Aristotle wrote the final statement and that he vouches for it because he had written nearly the same statement himself. The development follows an outline that proves $\log a/\log b$ irrational, uses the density of the fractional parts to bound the gaps between subset sums, builds an arithmetic progression of subset sums, and concludes completeness. It was not built or audited here, so the page lists no formalized evidence. A later quantitative claim by other authors has its own page, Song and Yue's bound on the exponent range.