Erdős problem 349

For $0 < \alpha \le 1$ and any $t > 0$ , $(t, \alpha)$ is not a good pair: every term $\lfloor t\alpha^n\rfloor$ lies in the finite interval $[0, \lfloor t\rfloor]$ (since $\alpha^n \le 1$ ), so every subset sum is bounded by the constant $\sum_{i \in [0,\lfloor t\rfloor]} i$ , and no large integer can be a subset sum. A partial result on the open Erdős Problem 349, complementing the $2 < \alpha$ and integer-coefficient cases.

Sources

The source's own material, retained exactly.

12 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

349.lean

Retained formal statement10 of 12

**Integer leading coefficient $t \ge 2$ blocks completeness.** For every integer base $\alpha$ , the pair $(t, \alpha)$ with integer $t \ge 2$ is not good: $\lfloor t\alpha^n\rfloor = t\alpha^n$ is a multiple of $t$ , so every subset sum is too, but two consecutive large integers cannot both be multiples of $t$ . Generalizes the parity obstruction ( $t = 2$ ). A partial result on Erdős Problem 349.

FormalConjectures/ErdosProblems/349.leanErdos349.int_coeff_ge_two_not_isGoodPair1 lineExact file

1∀ (t : ℤ), 2 ≤ t → ∀ (α : ℤ), ¬Erdos349.IsGoodPair ↑t ↑α

SolvedProof has a holeformal conjecturesexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.