Erdős Problem 1074

Exercise 1074 · Erdős

The formal statement below is all there is.

Formal statement · Lean 4.lean

theorem two_not_mem_pillaiPrimes : ¬ 2 ∈ PillaiPrimes := by
  sorry

Proof. sorry

Nobody has tried yet.