erdős #13
Let be such that there are no such that and . Is it true that ?
Worked, still open.
number theory · solved · prize $100 · formalized (Lean) · 0 attempts
machinery: consecutive-integer-window,additive-combinatorics,g_kr-divisors,extremal-set-system,prime-distribution
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsformal
AMS 5 11 · solved (literature)
theorem erdos_13 : ∃ C : ℝ, ∀ N : ℕ, ∀ A ⊆ Icc 1 N, IsForbiddenTripleFree A →
(A.card : ℝ) ≤ (N : ℝ) / 3 + Cformal-conjectures/13.lean ↗oeis
status
solved