Skip to content

Erdős problem 867

Is it true that if A={a1<⋯<at}⊆{1,…,N}A=\{a_1<\cdots <a_t\}\subseteq \{1,\ldots,N\} has no solutions to ai+ai+1+⋯+aj∈Aa_i+a_{i+1}+\cdots+a_j\in A then ∣A∣≤N2+O(1)?\lvert A\rvert \leq \frac{N}{2}+O(1)?

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

867.lean

Retained formal statement1 of 6

Is it true that if A={a1<⋯<at}⊆{1,…,N}A=\{a_1<\cdots <a_t\}\subseteq \{1,\ldots,N\} has no solutions to ai+ai+1+⋯+aj∈Aa_i+a_{i+1}+\cdots+a_j\in A then ∣A∣≤N2+O(1)?\lvert A\rvert \leq \frac{N}{2}+O(1)?

In fact this problem is false. Freud [Fr93] constructed a sequence with density ≥19/36\geq 19/36. The current best bounds are due to Coppersmith and Phillips [CoPh96], who prove that the maximal size of such an AA satisfies 1324N−O(1)≤∣A∣≤(23−1512)N+log⁡N.\frac{13}{24}N -O(1)\leq \lvert A\rvert \leq \left(\frac{2}{3}-\frac{1}{512}\right)N+\log N.

FormalConjectures/ErdosProblems/867.leanErdos867.erdos_8671 lineExact file
False ↔ ∃ C, ∀ (N : ℕ), ∀ A ⊆ Finset.Icc 1 N, Erdos867.ConsecutiveSumFree A → ↑A.card ≤ ↑N / 2 + C
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.