---

Claim. Let $\gamma=\sqrt\varphi\approx1.27202$, $\varphi$ the golden ratio. For every $u>0$ there is $L\in\mathbb Z$ such that every integer $z\ge L$ is $\sum_{i\in t}\lfloor\gamma^iu\rfloor$ for some finite $t\subset\mathbb N$. This is the theorem single_complete (line 316 of the pinned file) of Kenta Kitamura's Lean 4 repository, the result behind the Problem 354 claim page, whose card is kitamura_2026_lean_proof_erdos_problem_354_ii. For Problem 349 it says that the sequence $\lfloor t\alpha^n\rfloor$ is complete for every $t>0$ at the one base $\alpha=\sqrt\varphi$. The README states that the formalization was developed with assistance from ChatGPT and OpenAI Codex, using GPT-6 (Astra), the author's own disclosure.

Covers. Every pair $(t,\sqrt\varphi)$ with $t>0$ of the corrected Statement: with $u=t\alpha$ the theorem's sums over finite index sets are the Statement's sums of $\lfloor t\alpha^n\rfloor$, $n\ge1$, so the sequence is complete. Applied to the tail from which the terms are strictly increasing, the theorem also gives the site's wording, with values counted once and either index start. Completeness is proved on the line $\alpha=\sqrt\varphi$, so the claim's value is proved. It says nothing about any other base, and in particular nothing about the pairs with $t\ge\min(2/\alpha,3/\alpha^2)$ at other bases below the golden ratio, which remain open.

Claimant and postings. Kenta Kitamura (GitHub KitaKen1) published the repository on 2026-09-05 (the pinned revision) and announced the proof the same day in the site's thread of Problem 354, for whose catalog statement the theorem was written; the thread of Problem 349 does not mention it. The README reports kernel checks with no sorry and #print axioms giving propext, Classical.choice and Quot.sound, the author's own report.

Standing. Claimed: an unreviewed Lean development with only the author's axiom report; this corpus has not built it, so no formalized evidence is listed, and no refereed source, outside review or site mention of the result on Problem 349 exists.

Depends on. Nothing in this wiki.