True ↔ ∀ C > 0, ∃ K ≥ 3, {(a, b, n) | a > 0 ∧ b > 0 ∧ n > 0 ∧ ↑a + ↑b > ↑n + C * Real.log ↑n ∧ ∀ (p : ℕ), Nat.Prime p → p > K → padicValNat p (↑n.factorial / (↑a.factorial * ↑b.factorial)).den = 0}.Infinite