---

Claim. On 2026-06-19 Liam Price posted in the thread of Problem 346 a disproof whose argument GPT Pro produced as Price prompted, together with a Lean formalization completed by GPT-5.5 in Codex, as the site's proof-claim entry names the two systems; the write-up, whose author line names GPT Pro alone, is the preprint recorded on the card price_2026_counterexample_erdos_problem_346. Its Theorem 1 constructs a strictly increasing sequence $A=(a_n)$ of positive integers such that $A$ minus any finite subsequence is complete, $A$ minus any infinite subsequence is not complete, $a_{n+1}/a_n\ge 6/5$ for every $n$, and along an increasing index sequence $(N_j)$

$$\frac{a_{N_j}}{a_{N_j-1}}\to\varphi \qquad\text{and}\qquad \frac{a_{N_j+1}}{a_{N_j}}\to\varphi+\frac14,$$

with $\varphi=(1+\sqrt5)/2$. So the ratios $a_{n+1}/a_n$ do not converge, and the hypotheses of the question do not force the limit $\varphi$: the statement asked about is false, and the answer to the question as posed is no. The construction runs long stretches of Graham's recurrence $x_{n+2}=x_{n+1}+x_n-(-1)^n$, whose tails are all complete (the paper's Lemma 2), separated by sparse perturbations of size about $a_n/4$.

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

GPT Pro provides a counterexample. The Lean formalisation was completed by GPT-5.5 in Codex.

What is and is not settled. The thread disputes the reading of the question. A commenter suggested on 2026-06-19, and Nat Sothanaphan agreed on 2026-06-20, that the question likely assumes the limit of $a_{n+1}/a_n$ exists: the phrasing in Erdős and Graham's 1980 monograph is unclear, while Graham's 1964 paper asks whether the limit can differ from $\varphi$, and on that reading Price can be regarded as solving a variant problem. The problem's Statement, like Erdős and Graham's question, makes convergence part of the conclusion, and the counterexample refutes it in that form; the site's label describes that statement. The limit-exists reading is a variant. For it, Kenta Kitamura's Lean development of 2026-06-21, checked in the thread by the same reader, claims the answer yes: its theorems state that the deletion hypotheses, a uniform ratio gap and a limit $L>1$ force $L=\varphi$, and Sothanaphan notes that the case $L>\varphi$ also follows from Burr and Erdős (1981); it is recorded as the partial claim Kitamura's limit-exists theorem.

Formalization. The Lean proof, completed by GPT-5.5 in Codex, was first posted as code embedded in a live.lean-lang.org link in Price's thread post of 2026-06-19 and reposted in the comments of the site's proof-claim entry on 2026-07-15, whose own formalization field holds a cut-off copy of that link, as its comments record. The repository plby/lean-proofs holds a port of it to Lean 4.33.0, added 2026-08-26 (the formalization link, pinned to the port's last change of 2026-08-31), which describes itself as Liam Price and GPT-5.5's formalized proof claim and proves erdos_346_counterexample, a sequence with both deletion properties, ratios at least $6/5$, the two subsequential limits and no limit, and not_erdos_346, that the hypotheses do not force the ratios to converge to $\varphi$. Nothing was built or audited here, and no formalized evidence is listed.

Acceptance. Reviewed: Nat Sothanaphan reported in the thread on 2026-06-20 that, from a screening check, the Lean proof appears correct and corresponds to the paper, noting one typo in the proof of Lemma 3, and that they consider the result correct, while agreeing that the question likely assumes the limit exists (see above) and pointing to the 1981 paper of Burr and Erdős on perturbed complete sequences as a precursor whose results are similar to Price's but do not give them; the site's curator, T. F. Bloom, labels Problem 346 solved at erdosproblems.com and credits the counterexample to GPT Pro at Price's prompting, recording the sequence's ratio bound $6/5$ and its two subsequential limits (page last edited 1 September 2026). The site's proof-claim entry of 2026-07-15 names Liam Price as claimant and submitter (forum user Leeham) and the systems as GPT Pro and GPT 5.5, the Lean formalization completed by GPT-5.5 in Codex; its two comments of 2026-07-15, by a commenter and Price, concern the entry's formalization link, not the mathematics. Nothing here was checked by this project.