Skip to content

Problem

erdos:865

∃ 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

Declared status
proved (Lean)
Formalization
formalized
OEIS
possible

Matching claims

0
No direct claims
This problem has no directly related claim record.

Search problems.science

Find a Problem, Result, source, or page