There exists a constant $C > 0$ such that, for all large $N$ , if $A \subseteq {1, \dots, 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$ .

Worked, still open.

number theory · open · possible · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

What you wrote is (as far as I can tell from the current literature) **an open Erdős–Sós–type extremal problem**, listed as **Erdős Problem #865**. In particular, the existence of an absolute constant $C$ making the (\frac58N+C) threshold work for all sufficiently large $N$ is *not known* at present. ([Erdős Problems][…

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 5 11 · open (literature)

theorem erdos_865 :
    ∃ C > 0, ∀ᶠ (N : ℕ) in atTop,
      ∀ A ⊆ 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

formal-conjectures/865.lean ↗

status

open

evidence

formal

status

Search Vela