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,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 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,c∈Aa,b,c\in A such that a+b,a+c,b+c∈Aa+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 8∣A∣≤5N+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,    ∀ A ⊆ Finset.Icc 1 N,      ↑A.card ≥ 5 / 8 * ↑N + C → ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ a + b ∈ A ∧ a + c ∈ A ∧ b + c ∈ A
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.