Erdős Problem 203

Reference: erdosproblems.com/203

theorem erdos_203 : (∃ (m : ℕ), m.Coprime 6 ∧ ∀ (k l : ℕ), ¬Nat.Prime (2 ^ k * 3 ^ l * m + 1)) ↔ sorry

Is there an integer m with (m, 6) = 1 such that none of 2^k * 3^ℓ * m + 1 are prime, for any k, ℓ ≥ 0?