Skip to content

Erdős problem 865

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,cAa,b,c\in A such that a+b,a+c,b+cAa+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 statement1 of 4

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,cAa,b,c\in A such that a+b,a+c,b+cAa+b,a+c,b+c\in A.

A problem of Erdős and Sós (also earlier considered by Choi, Erdős, and Szemerédi [CES75], but Erdős had forgotten this).

This is true. The linked proof gives it in the contrapositive and with the constant cleared: every triple-free A{1,,N}A\subseteq\{1,\ldots,N\} satisfies 8A5N+C8\lvert A\rvert\leq 5N+C for a fixed CC, for every NN rather than only for large NN. It also shows the threshold is sharp, by exhibiting triple-free sets of size (5N+16)/8(5N+16)/8 for every NN divisible by 88.

FormalConjectures/ErdosProblems/865.leanErdos865.erdos_8654 linesExact file
C > 0,  ∀ᶠ (N : ℕ) in Filter.atTop,AFinset.Icc 1 N,A.card ≥ 5 / 8 * ↑N + C → ∃ aA, ∃ bA, ∃ cA, abacbca + bAa + cAb + cA
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.

Search problems.science

Find a Problem, Result, source, or page