lean_workbook_plus_75653

Disproved

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

Prove that an odd prime number $p$ can be represented in the form $x^2+2y^2$ if and only if $p=8k +1$ or $p=8k+3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75653 : ∀ p : ℕ, p.Prime ∧ p % 8 = 1 ∨ p.Prime ∧ p % 8 = 3 ↔ p.Prime ∧ ∃ x y : ℕ, x^2 + 2*y^2 = p   :=  by sorry

Source