Erdős problem 865 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

865.lean

Retained formal statement3 of 4

Erdős and Sós conjectured that $f_k(N)\sim \frac{1}{2}\left(1+\sum_{1\leq r\leq k-2}\frac{1}{4^r}\right) N$ , where $f_k(N)$ is the minimal size of a subset of $\{1, \dots, N\}$ guaranteeing $k$ elements have all pairwise sums in the set.

FormalConjectures/ErdosProblems/865.leanErdos865.erdos_865.variants.sos4 linesExact file

1∀ (k : ℕ),2  2 ≤ k →3    Asymptotics.IsEquivalent Filter.atTop (fun N => ↑(Erdos865.f N k)) fun N =>4      1 / 2 * (1 + ∑ r ∈ Finset.Icc 1 (k - 2), (1 / 4) ^ r) * ↑N

OpenStatement only, no proof

Sources

Search problems.science