Erdős problem 867
Is it true that if has no solutions to then
Sources
FormalConjectures/ErdosProblems/
867.lean
Retained formal statement
Is it true that if has no solutions to then
In fact this problem is false. Freud [Fr93] constructed a sequence with density . The current best bounds are due to Coppersmith and Phillips [CoPh96], who prove that the maximal size of such an satisfies
False ↔ ∃ C, ∀ (N : ℕ), ∀ A ⊆ Finset.Icc 1 N, Erdos867.ConsecutiveSumFree A → ↑A.card ≤ ↑N / 2 + C