---

Claim. Let $\alpha$ be a positive rational, $L\ge1$ an integer, and $p\in\mathbb Q[x]$ a polynomial that takes integer values at the integers, has positive leading coefficient, and has no fixed divisor $d\ge2$ of its values at the positive integers. Then there is $m_0$ such that every integer $m\ge m_0$ can be written as $m=p(n_1)+\cdots+p(n_k)$ with integers $L<n_1<\cdots<n_k$ and $\alpha=1/n_1+\cdots+1/n_k$. The case $\alpha=1$, $L=1$ is the question of Problem 283 for every admissible polynomial, so the claim answers it yes; the general $\alpha$ is the strengthening Graham conjectured in 1963, and the same argument settles Problem 351 in its corrected form.

Depends on. No page of this wiki; the argument's one external input is Theorem 1 of Graham's 1964 paper on complete sequences of polynomial values, whose library card the outline below links; the card has no result page for it.

Claimant and provenance. The argument was generated by the AI system GPT 5.5 Pro at the prompting of Liam Price, who posted it in the site's discussion thread on 3 May 2026 with a writeup on Overleaf; Kevin Barreto edited the writeup, keeping the changes minimal, and noted that the corrected Problem 351 follows. A revised presentation of 6 May 2026 ("Polynomial Egyptian Sums: a formalization-informed revised presentation", 13 pages, linked from the thread as a Google Drive file) states the result as its Theorem 8 (p. 4), names the Roth--Szekeres--Graham completeness theorem as its only external input, and lists in its Appendix A the presentation changes made for the formalization, with the proof strategy unchanged. Price, who submitted the result, is the claimant; the system that generated the argument is named above.

The argument in outline. With $p(x)=cx^d+\cdots$, put $u_j=36j+1$ and $D_j=u_ju_{j+1}$, so that $\frac1{36}=\sum_{0\le j<J}\frac1{D_j}+\frac1{36u_J}$ by telescoping. Replacing a denominator $D_j$ by the three denominators $2D_j,3D_j,6D_j$ keeps the reciprocal sum (since $1=\frac12+\frac13+\frac16$) and the distinctness, and changes the $p$-sum by $q(j)=p(6D_j)+p(3D_j)+p(2D_j)-p(D_j)$, a polynomial in $j$ of degree $2d$ with positive leading coefficient. Graham's completeness theorem of 1964 (Theorem 1 of that paper) gives $g$ and $X$ such that every multiple of $g$ that is at least $X$ is a sum of distinct values $q(j)$. Finite sets $A_k$ of denominators with reciprocal sum $1-\frac1{36}$, avoiding the residues $0,1,2,3,6$ modulo $36$ and with $\sum_{a\in A_k}p(a)\equiv k\pmod g$, supply the residue classes; the $p$-sum of the base representation built from $D_0,\ldots,D_{J-1}$, $36u_J$ and $A_k$ rises by about $c\,36^{2d}J^{2d}$ from $J$ to $J+1$, less than $q(J)$, which is about $c(6^d+3^d+2^d-1)\,36^{2d}J^{2d}$, so for a large target $m$ in the class $k$ there is a $J$ whose deficit $m$ minus the base $p$-sum lies between $X$ and $q(J)$; Graham's theorem writes that deficit as a sum of distinct $q(j)$, which must have $j<J$, and switching those $D_j$ reaches $m$. This outline follows the curator's summary in the thread (10 May 2026), with its constants corrected as the problem page records, and the manuscript's statement; no step is verified.

Acceptance. The site's curator, Thomas Bloom, marked the problem PROVED (LEAN) on 10 May 2026, credited the argument in the problem's commentary, and posted a summary of the proof in the thread, which is the reviewed evidence: an acceptance independent of the claimant. In the same thread, Nat Sothanaphan summarized the argument's structure on 3 May 2026 and reported on 6 May 2026 that they had confirmed the proof. The community database at teorth/erdosproblems lists the problem as proved (Lean), as of its last update of 10 May 2026. No refereed publication, arXiv posting or review outside the site's thread was found in the search of 2026-09-18 recorded on the problem page.

Formalization. The file Erdos/P283/Proof_flat.lean of the repository Shashi456/erdos-formalizations, at the pinned commit of the first formalization link (11,229 lines, one import Mathlib, no sorry and no axiom declaration), declares itself a formalization of this argument and attributes the informal proof to the AI system with the human cleanup; its theorem_1 states the claim above with IntValued p and NoFixedDivisor p hp for the hypotheses on $p$, and the file proves its completeness input from Graham's 1964 paper rather than assuming it (the formalizer's report of 6 May 2026 in the thread). The formal-conjectures statement file ErdosProblems/283.lean points at this file through its formal_proof attribute; it is a statement with proof sorry and is not a formalization of the result. A second file, src/latest/ErdosProblems/Erdos283.lean of Boris Alexeev's repository plby/lean-proofs at the pinned commit of the second formalization link (211 lines), declares itself a formalization of a solution to Problem 283, names GPT-5.5 Pro and Liam Price as its informal authors and the AI systems Opus 4.7 and GPT-5.5 Pro with Pawan Sasanka Ammanamanchi as its formal authors, proves erdos_283 : ∀ p : ℤ[X], Condition p (a statement over integer-coefficient polynomials, narrower than the integer-valued polynomials of the site's statement and of the formal-conjectures Condition, which include for example $x(x+1)/2+1$) without sorry with the recorded axioms propext, Classical.choice and Quot.sound, and links the Shashi456 file and the formal-conjectures statement. Nothing was built or kernel-checked by this corpus, and the fidelity of either theorem to the site's statement is not audited, so the claim lists no formalized evidence; the formalization links record where the Lean proofs are.

Special cases. Three partial claims, Graham's accepted and Alekseyev's and van Doorn's pending, address instances of the problem and have their own pages: Graham's Theorem 1 of 1963, the case $p(x)=x$ (every $m>77$, with $77$ excluded; refereed; Graham 1963); Alekseyev's Theorem 1 of 2019, the case $p(x)=x^2$ (every $m>8542$, sharp; a published book chapter; Alekseyev 2018); and van Doorn's binomial-case manuscript, the families $x+b$ ($1\le b\le5000$), $5x+b$ ($1\le b<375$, $5\nmid b$) and $x^2+b$ ($1\le b\le800$) (van Doorn 2025). The general claim above does not rest on them.