lean_workbook_plus_62702

Proved

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

Let $p$ be a prime number such that $p \mid a^2 + 2$ for a natural number $a$ . Prove that $p$ or $2p$ can be written on the form $x^2 + 2y^2$ , with $x,y \in \mathbb{N}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_62702 (p a : ℕ) (hp : Nat.Prime p) (hpa : p ∣ a^2 + 2) : ∃ x y : ℕ, p ∣ x^2 + 2*y^2 ∨ 2*p ∣ x^2 + 2*y^2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph