certified
For positive alpha and beta with irrational ratio, every sufficiently large integer is a finite sum of indexed terms from the sequences floor(2^n alpha) and floor(2^n beta). This establishes part (i), with the intended multiset interpretation.
Submitted by JenW1N
Certified 16 Sept 2026, published by conjectures.io.
Review decision
Approved in reviewREVIEW_APPROVED
Approved under REVIEW_APPROVED pursuant to manual-review policy v3. The submission was accepted on 11 September 2026 at 20:48:55.093075 UTC and proves the affirmative answer to Erdős Problem 354(i): for every positive α and β with irrational ratio, every sufficiently large integer is a finite sum of indexed terms from the sequences ⌊2ⁿα⌋ and ⌊2ⁿβ⌋. The accepted Lean statement preserves the intended multiset interpretation and includes every exponent. The exact committed target and proof passed verification with only the permitted standard axioms. The review found no qualifying earlier public solution substantially used for this target, or earlier completed external formalization of it. The recent formalization of part (ii) uses a base below 2 and does not prove part (i). Fan's September 2026 completeness criterion leaves the relevant two-ray case unresolved. The located full proof claim posted on September 13, with a linked repository created September 12, is later than acceptance. These findings are bounded by the sources inspected, including some unavailable full texts and incomplete social-search coverage; they are not a guarantee of absolute novelty. The full locked conjecture bounty applies. The submitter may request reconsideration and provide contrary chronology, source-correspondence or formalization evidence. Sources: [Erdős Problem 354](https://www.erdosproblems.com/354), [Fan v4](https://arxiv.org/abs/2607.14071v4), [part-II formalization](https://github.com/KitaKen1/erdos-354-part-ii), [later proof claim](https://www.erdosproblems.com/forum/thread/354/proof-claims), [review policy](https://github.com/conjectures-io/conjectures-validator/blob/076ead3c71c8b0bfc0641975076d95015d075ce3/docs/MANUAL_REVIEW_CRITERIA.md).
Approved · decided 15 Sept 2026
Formal statement
True ↔ ∀ α > 0, ∀ β > 0, Irrational (α / β) → IsAddCompleteNatSeq' (Erdos354.FloorMultiples.interleave α β 2)Verification report
Every box below had to hold before the proof counted. They are grouped in the order the verifier reaches them.
Manifest valid — Passed
The task bundle held together: the exact file set, a strict manifest, and every trusted hash matching the bytes on disk.
Task commitment matches — Passed
The bundle digest the submission committed to is the digest of the bundle that was actually verified.
Production task — Passed
The task came from the production pool rather than a test fixture.
Trusted file hashes match — Passed
The pinned dependencies agree across the manifest, the lockfile and the checkout, down to the same Formal Conjectures commit.
Submission policy respected — Passed
The submitted source passed the static scan: no imports, no axiom declarations, no sorry, no native_decide, no unsafe options.
Production sandbox — Passed
The run happened under real isolation, Landrun with seccomp, and the sandbox passed its own live self-test before the proof was touched.
Challenge built — Passed
The trusted Challenge.lean, which contains no miner code, compiled on its own.
Source type hash matches — Passed
The source theorem in the compiled environment still hashes to the type recorded in the task, so the statement has not drifted upstream.
Solution built — Passed
The submitted Solution.lean compiled.
Statement unchanged — Passed
The theorem the proof establishes has exactly the same canonical type as the task's target - it was not weakened or restated.
Only permitted axioms — Passed
The transitive axiom closure of the proof stays inside the axioms this task permits.
Lean kernel accepted — Passed
The Lean kernel replayed the proof and accepted it.
Nanoda accepted — Not run
A second kernel, written independently of Lean's, also accepted the proof.
One kernel, not two
This task does not require a second, independent kernel, so Nanoda was not run. The verdict rests on a single kernel implementation.
Theorems established
Stage COMPLETED · Axioms permitted: propext, Quot.sound, Classical.choice