Erdős problem 867
Is it true that if has no solutions to then
Sources
FormalConjectures/ErdosProblems/
867.lean
Retained formal statement
Freud [Fr93] constructed a sequence with density .
∀ (ε : ℝ), 0 < ε → ∀ᶠ (N : ℕ) in Filter.atTop, ∃ A ⊆ Finset.Icc 1 N, Erdos867.ConsecutiveSumFree A ∧ (19 / 36 - ε) * ↑N ≤ ↑A.cardSolvedStatement only, no proof