Erdős problem 867
Is it true that if has no solutions to then
Sources
FormalConjectures/ErdosProblems/
867.lean
Retained formal statement
Adenwalla has observed that
∀ (ε : ℝ), 0 < ε → ∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, Erdos867.ConsecutiveSumFree A → ↑A.card ≤ (2 / 3 + ε) * ↑NSolvedStatement only, no proof