Skip to content

Erdős problem 865

Start work

There exists a constant C>0C>0 such that, for all large NN, if A⊆{1,…,N}A\subseteq \{1,\ldots,N\} has size at least 58N+C\frac{5}{8}N+C then there are distinct a,b,c∈Aa,b,c\in A such that a+b,a+c,b+c∈Aa+b,a+c,b+c\in A.

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

865.lean

Retained formal statement2 of 4

It is a classical folklore fact that if A⊆{1,…,2N}A\subseteq \{1,\ldots,2N\} has size ≥N+2\geq N+2 then there are distinct a,b∈Aa,b\in A such that a+b∈Aa+b\in A, which establishes the k=2k=2 case.

FormalConjectures/ErdosProblems/865.leanErdos865.erdos_865.variants.k21 lineExact file
∀ (N : ℕ), ∀ A ⊆ Finset.Icc 1 (2 * N), A.card ≥ N + 2 → ∃ a ∈ A, ∃ b ∈ A, a ≠ b ∧ a + b ∈ A
SolvedStatement only, no proof