Claim. For all $\alpha,\beta>0$ with $\alpha/\beta$ irrational, every sufficiently large integer is

for some finite $S,T\subset\mathbb N$: the first question of Problem 354, answered yes in the site's own reading, where indices rather than values are used at most once, so equal values at different indices count separately and zero terms are harmless. The theorem proved is the catalog statement Erdos354.erdos_354.parts.i with its answer instantiated to true,

True ↔ ∀ α > 0, ∀ β > 0, Irrational (α / β) →
  IsAddCompleteNatSeq' (Erdos354.FloorMultiples.interleave α β 2)

whose interleave α β 2 is the sequence $\lfloor\alpha\rfloor,\lfloor\beta\rfloor,\lfloor2\alpha\rfloor,\lfloor2\beta\rfloor,\ldots$, whose subseqSums' sums over finite index sets, and whose IsAddCompleteNatSeq' asks that every sufficiently large integer be such a sum; a finite index set is exactly a pair $(S,T)$. The proof's reduction chain, as the file (10,152 lines) presents it: a scaling to $\alpha,\beta\ge1$, then two criteria on the binary digits of $\alpha$ and $\beta$, whose joining and disjointness argument on the digit sequences (about 9,000 lines) rests on the site's kernel acceptance. The result page target unfolds the accepted theorem to the site's wording, and the source card jenw1n_2026_erdos_354_part_i_lean_proof records the site's solution file.

Covers. The first question only: base $2$, the irrational-ratio hypothesis, indexed (multiset) sums, every exponent included. It makes no strong-completeness or set-union claim, says nothing about the second question (a base $\gamma\in(1,2)$ in place of $2$), and leaves the rational-ratio cases of Hegyvári's conjecture untouched.

Claimant and posting. The bounty site credits the proof to the solver handle JenW1N; the file's header names no author and declares no AI system, and no paper, preprint or write-up accompanies it. The site shows the proof as verified, the earliest date the record carries, which names this page. The same result in a stronger form was later claimed by Yu and Chen (manuscript of 13 September 2026, repository created 12 September), whose own page is the Yu–Chen claim page; the site's review notes that claim as later than its acceptance.

Acceptance. Reviewed: the bounty site Conjectures.io's documented acceptance of the exact statement, which is the reviewed evidence named here. Its Lean kernel accepted the proof on 11 September 2026 with propext, Quot.sound and Classical.choice as the only permitted axioms, its static scan found no imports, axiom declarations, sorry, native_decide or unsafe options, its report records that the theorem proved has exactly the task's canonical type, its manual review approved the record on 15 September 2026 under its review policy v3 after a prior-art check that found no earlier public solution, and the record was certified on 16 September 2026 with the bounty paid. The site's second, independent kernel was not run, so the kernel verdict rests on one implementation, and the review's note says its novelty findings are bounded by the sources it inspected. No formalized evidence is listed: this corpus has not built or replayed the file, which redefines none of the catalog's names. No refereed evidence exists, and on 2026-09-28 the erdosproblems.com page labeled the problem OPEN, its proof-claims tab listed the Yu–Chen claim and not this record, and the formal-conjectures catalog kept parts.i research open. The catalog commits pinned on the record page and in the task bundle were not publicly retrievable on 2026-09-28; the identity of the pinned statement rests on the task bundle's printed type, the shared source type hash and the proof's own use of the corrected interleave definition.

Depends on. Nothing in this wiki; the claim is the Lean theorem the bounty site accepted.