---

Claim. For every integer $d\ge5$ there is a computable set $A_d\subseteq\mathbb Z$ such that every integer $m$ has exactly one representation $m=a+n^d$ with $a\in A_d$ and an integer $n\ge0$. For $d=6$ the set $\{n^6:n\ge0\}$ is the full image $\{n^6:n\in\mathbb Z\}$, so the claim answers Problem 477 affirmatively with $f(X)=X^6$. Liam Price submitted the claim on 27 July 2026, naming the system GPT 5.6 Sol Pro in the claim's tool field; the claim's summary calls it GPT Pro and the curator's exposition GPT 5.6 Sol.

Submission note. Posted to erdosproblems.com as a proof claim by Liam Price (account Leeham) on 27 July 2026, giving "GPT 5.6 Sol Pro" as the AI used:

GPT Pro constructs, for every integer $d\geq 5$, a computable set $A_d\subseteq\mathbb Z$ such that every integer has a unique representation

$$m=a+n^d, \qquad a\in A_d,\quad n\geq 0.$$

Taking $d=6$, we

obtain

$$\mathbb Z=A_6\oplus\{n^6:n\in\mathbb Z\},$$

thereby answering the

all-integer formulation in the affirmative. Notes: I've had this solution for a while, and although I believe I obtained this proof first, it is important to note this solution was posted before I got the chance to submit. Since I haven't seen it mentioned here yet, I thought I'd show both.

Acceptance. The site's curator, Thomas Bloom, marked the problem solved on 5 September 2026. Bloom's commentary credits GPT, prompted independently by Price and by pipeline-math, with proving that such an $A$ exists for $f(n)=n^d$ and every even $d\ge6$, and Bloom's signed exposition of the same day expounds Price's construction. That credit is the reviewed evidence here, and it covers the even exponents $d\ge6$, for which $\{n^d:n\ge0\}$ is the full image $f(\mathbb Z)$; the exponent $d=6$ settles the problem. The case $d=5$ and the odd exponents $d\ge7$ with nonnegative inputs, which the claim also asserts, rest on the claimant alone: no source credits them, and the exposition treats positive inputs only. No journal publication or arXiv posting is known.

Qualification. The linked Overleaf manuscript showed only its application shell at the shared link in the status search, so this page does not rest on its proof and the link is unpinned. The exposition writes the tiled set as $\{n^d:n\ge1\}$, with positive inputs, while this claim names $\{n^d:n\ge0\}$; the two sets differ by the element $0$ for every $d$, and for even $d$ the claim's set is the full image $\{n^d:n\in\mathbb Z\}$, so the exposition's theorem is not by itself a proof of this statement, and the acceptance rests on the curator's credit rather than on a review of the manuscript. The problem is settled independently by the thirteenth-power construction on its claim page.

Formalization. Erdos477.lean in Boris Alexeev's repository, linked above at its pinned commit, declares itself an affirmative answer to Problem 477 with $f(X)=X^6$ whose informal source is Price's manuscript Large Powers Tile the Integers, with GPT 5.6 Sol Pro named beside Price, and whose formal author is Codex; its header says that the determinant and curve estimates are developed unconditionally, that uniqueness is of the two summand values and not of a polynomial input, and that the greedy criterion also appears in the pipeline-math manuscript. It is a formalization of this result and so a link on this page, not a separate claim. The formal-conjectures statement file marks its statement erdos_477 research solved with a formal-proof link to that file, and its monomial variant likewise. This repository has not built or audited the file, so it is not formalized evidence.