---

Claim. Let $S_k$ be the set of natural numbers that are a prime plus at most $k$ powers of $2$, with the summand $2^0=1$ and repeated powers allowed. The even numbers outside $S_3$ form an infinite set. In Lean this is the catalog's Erdos10.erdos_10.variants.grechuk, Set.Infinite ({n | Even n} \ Erdos10.sumPrimeAndTwoPows 3). The result is the parenthetical remark of the site's commentary on Problem 10, credited there to Bogdan Grechuk, made a theorem; the write-up's first paragraph says that it does not resolve the question, which asks whether one fixed number of powers of $2$ suffices for every sufficiently large integer. What it shows about the question is that $k=3$, and so every $k\le3$, fails, so any $k$ answering it yes is at least $4$. Since the question asks whether some $k$ exists, the result is a partial no, the answer no for every $k\le3$, which the claim value records; it does not decide whether a larger $k$ exists.

Submission note. Posted to erdosproblems.com as a proof claim by R. Crocker (underlying construction); Daryxx (Lean formalisation and Grechuk-variant bridge) (account Daryxx) on 7 August 2026, giving "OpenAI GPT-5.6 Sol; OpenAI GPT-5.6 Terra; Claude Fable 5" as the AI used:

Let S_k be the natural numbers representable as a prime plus at most k powers of two, allowing exponent zero and repetitions. The claim is that infinitely many even natural numbers lie outside S_3; this is the Grechuk variant in the remarks, not a solution of the main Problem 10 question. Crocker's 1971 covering-congruence construction gives infinitely many distinct odd t > 15 with t congruent to 15 modulo 16 and t outside S_2 (after closing the exponent-zero and equal-exponent boundary cases). Put N = t + 1. If a representation of N in S_3 contains 2^0 = 1, removing it would put t in S_2. Otherwise all power-of-two terms are even, so the prime must be 2 and t - 1 would be a sum of at most three powers of two. But t - 1 is congruent to 14 modulo 16, which forces that sum to be exactly 2 + 4 + 8 = 14, contradicting t > 15. Thus every such N is even and outside S_3, and the injective shift gives infinitely many examples. Notes: The linked gist contains both a human-readable proof and the complete 2,289-line Main.lean formalisation. Its exact target is Set.Infinite ({n : ℕ | Even n} \ Erdos10.sumPrimeAndTwoPows 3), and the Lean file has SHA-256 784bb738d147dd8b6ad44e1ebf23004a5318cd9f47d4e40185b45209788e1c1d. Lean 4.27 accepted it in the Conjectures.io production sandbox: https://conjectures.io/results/ce95887b-8b61-4a89-9069-9131a58906e0 . Conjectures.io later classified that independently developed formalisation as a duplicate of an earlier accepted submission for the same formal target. No priority or reward claim is made. Reference: R. Crocker, Pacific J. Math. 36 (1971), 103–107, https://doi.org/10.2140/pjm.1971.36.103 .

Covers. The site's parenthetical remark that infinitely many even integers cannot be written as a prime plus at most three powers of $2$, in the convention of the catalog's sumPrimeAndTwoPows (exponent zero and repeated exponents allowed, which only enlarges the representable set); hence the lower bound $k\ge4$ on any $k$ answering the question. Whether any $k$ exists is untouched.

Argument. A parity bridge from Crocker's construction (Crocker 1971, Theorem I), which gives infinitely many distinct odd $t>15$ with $t\equiv15\pmod{16}$ and $t\notin S_2$; Crocker states the exclusions for positive exponents, and the write-up closes the exponent-zero and equal-exponent boundary cases inside the construction. For each such $t$ put $N=t+1$, which is even. A representation of $N$ in $S_3$ containing the summand $1$ would, after one $1$ is removed, put $t$ in $S_2$; otherwise every power-of-two term is even, so the prime is $2$ and $t-1\equiv14\pmod{16}$ is a sum of at most three powers of $2$, which a residue check forces to be $2+4+8$, contradicting $t>15$. The map $t\mapsto t+1$ is injective, so the exceptions are infinite. The Lean file (2,289 lines) assembles Crocker's family by the Chinese remainder theorem over a table of $28$ residue classes on the exponent and closes the catalog's target by exact against its own CrockerCRTAssembly.erdos10_grechuk; the source card daryxx_2026_erdos_problem_10_grechuk_partial_result records the write-up and identifies the Lean file by size and final theorem.

Claimant and postings. The gist was created on 2026-08-07 under the handle Daryxx (GitHub login DaryxXx), the name the solution carries on the gist and on the site's proof-claims thread; its write-up's closing paragraph states that the Lean development was produced with substantial assistance from OpenAI GPT-5.6 Sol and GPT-5.6 Terra, with independent review by Claude Fable 5, the author's own disclosure. The same day the author registered the result on the erdosproblems.com proof-claims thread as a partial claim linking the gist as both proof and formalization. The Lean file had been submitted to the bounty site Conjectures.io the day before, as record ce95887b-8b61-4a89-9069-9131a58906e0 against the task for the catalog variant, and the site's kernel accepted it on 6 August 2026 (11:24:37 UTC); the site credits that record to an abbreviated solver address, and the claimant's own notes on the proof-claims thread identify it as the claimant's file, so that record is the first posting of the result and dates this page.

Acceptance. None listed as evidence. The formal-conjectures catalog's maintainers merged PR #5998 on 2026-09-14, which marks erdos_10.variants.grechuk research solved and cites this gist as the variant's formal_proof; this is catalog agreement with the variant, listed above as a record link, not a named outside review of the proof, and the catalog keeps the question itself research open. The bounty site Conjectures.io did not accept this record: its Lean kernel rebuilt the file in its sandbox and accepted the exact published target on 6 August 2026 (11:24:37 UTC), with the same verification checklist as for its certified record (static scan clean, statement unchanged, axioms inside propext, Quot.sound and Classical.choice, second kernel not run), but its review then set the record aside as a duplicate of an earlier submission for the same target, one reward being paid per target under its policy, and not on mathematical grounds, so this record carries no certification and no reward. The site's own certified acceptance of the variant is the earlier record 244ff2d0-399d-4e37-a307-4ff6f3cb3493, a different solver's Lean proof of the same formal statement, kernel accepted, review approved and certified on 6 August 2026, which has its own accepted claim page, the certified Conjectures.io proof; the write-up describes this file as independently developed, the source's own statement. The erdosproblems.com thread lists the claim under the site's disclaimer and records no acceptance. The corpus has not built or replayed the file, and the basis here is its text (final theorem, target type and tokens), so no formalized evidence is listed, and no refereed evidence exists. The variant was not open when the bounty site offered it: the site withdrew the target the same day as solved and not open, since the statement already follows from Crocker's published theorem by the parity reduction.

Depends on. Crocker 1971, Theorem I, the result page of Crocker's refereed theorem; the claim also rests on the Lean file the bounty site's kernel accepted.