Erdős Problem 12

Theorem 12 · Erdős

The set of $p ^ 2$ where $p \cong 3 \mod 4$ is prime is an example of a good set. Formal proof provided by AlphaProof

Formal statement · Lean 4.lean

theorem isGood_example :
    IsGood {p ^ 2 | (p : ℕ) (_ : p ≡ 3 [MOD 4]) (_ : p.Prime)} := by
  sorry

Proof. sorry

Nobody has tried yet.