Erdős problem 867
Is it true that if has no solutions to then
Sources
FormalConjectures/ErdosProblems/
867.lean
Retained formal statement
The current best bounds are due to Coppersmith and Phillips [CoPh96], who prove that the maximal size of such an satisfies
∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, Erdos867.ConsecutiveSumFree A → ↑A.card ≤ (2 / 3 - 1 / 512) * ↑N + Real.log ↑NSolvedStatement only, no proof