---

Claim. For $\alpha,\beta>0$ put $A_{\alpha,\beta}=\{\lfloor2^n\alpha\rfloor,\lfloor2^n\beta\rfloor:n\in\mathbb N\}\setminus\{0\}$. If $\alpha/\beta$ is irrational then for every finite $F\subset\mathbb Z$ there is an integer $H$ such that every integer $m\ge H$ is a sum of distinct elements of $A_{\alpha,\beta}\setminus F$; that is, $A_{\alpha,\beta}$ is strongly complete. The manuscript notes that this implies the indexed statement of the first question of Problem 354 (each index used at most once, equal values at different indices allowed) and that its theorem is the stronger distinct-values form. The result page Theorem states it, and the source card yu_chen_2026_erdos_problem_354_i_strong_completeness_two_dyadic_floor_sequences records the manuscript.

Submission note. Posted to erdosproblems.com as a proof claim by Yingzhe Yu, Kani Chen (account Andrewy) on 13 September 2026, giving "Chatgpt-6 Astra" as the AI used:

We prove that, for all positive real numbers $\alpha,\beta$ with irrational ratio, the nonzero values of $\lfloor2^n\alpha\rfloor$ and $\lfloor2^n\beta\rfloor$ form a strongly complete set: after any finite deletion, every sufficiently large integer is a sum of distinct remaining values. This answers Erdős Problem 354(i). An explicit finite coefficient certificate produces integer meshes whose gap bounds persist through subsequent layers and changes of modulus. Under incompleteness, these meshes yield permanent descent of a modular gap invariant, forcing bounded ratios between consecutive binary-event positions. Finite-event decay and digit-budget estimates produce sparse rational-approximation windows. Compactness of ratios of sparse binary sums then supplies a lower bound on return costs, which a counting argument shows to be incompatible with the event-spacing constraint.

Covers. The first question, in a strong-completeness form that implies the site's indexed answer yes; base $2$ and the irrational-ratio case only. The manuscript says that the rational-ratio cases of Hegyvári's conjecture and the variable-base second question are different statements and does not address them.

Argument. As the manuscript outlines it: normalize by powers of $2$, deleting only finite prefixes, so that $N=\lfloor\beta\rfloor<M=\lfloor\alpha\rfloor<2N$ with $N\ge2$, after which the two sequences interleave in sorted order with each weight at most twice its predecessor; index events by the layers at which a binary digit pair is nonzero, infinitely many since a finite event set would make $\alpha$ and $\beta$ dyadic rationals and so their ratio rational; build finite integer meshes from a certificate of twelve coefficient chains whose gap bounds persist through later layers and changes of modulus; show that under incompleteness long intervals between events force a modular gap invariant to descend for good, while finite-event decay and a digit-budget estimate give sparse rational-approximation windows; and close with a compactness bound on ratios of sparse binary sums and a counting argument against the event-spacing bound. This outline is a reading aid, not proof coverage.

Claimant and postings. Yingzhe Yu and Kani Chen, the authors the manuscript and the site's proof-claims entry name; the entry was submitted on 2026-09-13 under the forum handle Andrewy, and the repository Andrewyzzz/erdos354 was created on 2026-09-12. The manuscript states that the mathematical development and the Lean formalization were carried out with assistance from ChatGPT and OpenAI Codex, using GPT-6 (Astra), the source's own disclosure. The links are pinned to the repository's revision of 2026-09-20, its head on 2026-09-28, whose commit message records no proof changes since the manuscript's date. The authors opened formal-conjectures issue #6431 and PR #6433 on 2026-09-20 to record an affirmative part (i) from this repository.

Formalization. The repository's own account, which this corpus has not replayed: Lean 4.27.0 with pinned Mathlib; final theorems Dyadic354.erdos354_part_i and Dyadic354.erdos354_strong_completeness; an adapter reproducing the catalog's definitions from a pinned formal-conjectures revision, in which Dyadic354.UpstreamBridge.erdos354_part_i_upstream and erdos354_strong_upstream are proved; a results file reporting 381 theorems audited with every transitive axiom set inside propext, Classical.choice and Quot.sound and no sorry, custom axiom or native_decide. This corpus has not built the project or audited its statements, so the formalization is a link, not a warrant.

Standing. Claimed, with no acceptance evidence: no review, no referee, no site acceptance (the proof-claims tab lists the entry under the site's notice that appearing there is no guarantee of correctness, with no comments) and no catalog agreement (PR #6433 open and unmerged). The first question already has an accepted answer, the bounty site's certified Lean proof credited to JenW1N (its claim page), which the site's review dates two days before this manuscript; this claim is stronger than that answer and independent of it, and it changes no standing.

Depends on. Nothing in this wiki.