Erdős problem 13
If is a set with no such that and , then . This has been solved by Bedert [Be23].
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/13.lean∃ C, ∀ (N : ℕ), ∀ A ⊆ Finset.Icc 1 N, Erdos13.IsForbiddenTripleFree A → ↑A.card ≤ ↑N / 3 + CSolvedStatement only, no proof