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
∃ C, ∀ (N : ℕ), ∃ A ⊆ Finset.Icc 1 N, Erdos867.ConsecutiveSumFree A ∧ 13 / 24 * ↑N - C ≤ ↑A.cardSolvedStatement only, no proof