Odd prime divisors of $x^2+1$ have the form $4k+1$

Proved

AlfutovaUstinov.problem_4_126

by evgeth · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

elementary-number-theorynumber-theoryquadratic-residuessums-of-squares

This is Problem 4.126 of N. B. Alfutova and A. V. Ustinov, Algebra and Number Theory (MCCME, 2002), Chapter 4, §4 “Theorems of Fermat and Euler”.

Theorem. Let $x$ be an integer and let $p$ be an odd prime such that

p \mid x^{2}+1 .

Then $p$ has the form $p=4k+1$ for some natural number $k$ .

This classical fact (the only prime divisors of $x^2+1$ are $2$ and primes $\equiv 1 \pmod 4$ ) is used in the book's next problem to prove that there are infinitely many primes of the form $4k+1$ .

Formalization Note The prime $p$ is a natural number with Nat.Prime p and Odd p; the integer $x$ is arbitrary and divisibility is taken in $\mathbb Z$ .

Preamble

import Mathlib

Formal statement

namespace AlfutovaUstinov

theorem problem_4_126 (p : ℕ) (hp : p.Prime) (hodd : Odd p) (x : ℤ) (hx : (p : ℤ) ∣ x ^ 2 + 1) :
    ∃ k : ℕ, p = 4 * k + 1 := by sorry

end AlfutovaUstinov

Source

N. B. Alfutova, A. V. Ustinov, «Алгебра и теория чисел. Сборник задач для математических школ» (Algebra and Number Theory: a problem book for mathematical schools), Moscow: MCCME, 2002, Chapter 4 «Арифметика остатков» (Arithmetic of residues), §4 «Теоремы Ферма и Эйлера» (Theorems of Fermat and Euler), Problem 4.126. Problem text and answer as catalogued on problems.ru, problem 60752: https://problems.ru/view_problem_details_new.php?id=60752

View graph

Odd prime divisors of x2+1x^2+1x2+1 have the form 4k+14k+14k+1

Odd prime divisors of $x^2+1$ have the form $4k+1$