lean_workbook_plus_78200

Disproved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $n\equiv4\pmod8$ and $p$ is a prime factor of $n+2$ . Prove that $n\equiv 3\pmod4$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78200 (n : ℕ) (hn : n ≡ 4 [ZMOD 8]) (p : ℕ) (hp : p.Prime) (h : p ∣ (n + 2)) : n ≡ 3 [ZMOD 4]   :=  by sorry

Source