Prove2Me

There are infinitely many primes of the form 4k+14k+1

Proved
AlfutovaUstinov.problem_4_127

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

elementary-number-theoryinfinitude-of-primesnumber-theoryprimes-in-progressions

This is Problem 4.127 of N. B. Alfutova and A. V. Ustinov, Algebra and Number Theory (MCCME, 2002), Chapter 4, §4 “Theorems of Fermat and Euler”. (In the book the problem is to be solved with the help of the preceding Problem 4.126.)

Theorem. There are infinitely many prime numbers of the form

p=4k+1,k∈N.p = 4k+1, \qquad k\in\mathbb N .

This is the simplest nontrivial special case of Dirichlet's theorem on primes in arithmetic progressions, and it admits an elementary Euclid-style proof.

Formalization Note The statement says that the set {p∈N:p is prime and p=4k+1 for some k∈N}\{p\in\mathbb N : p \text{ is prime and } p=4k+1 \text{ for some } k\in\mathbb N\} is infinite (Set.Infinite).

Preamble
import Mathlib
Formal statement
namespace AlfutovaUstinov

theorem problem_4_127 : {p : ℕ | p.Prime ∧ ∃ k : ℕ, p = 4 * k + 1}.Infinite := 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.127. Problem text and answer as catalogued on problems.ru, problem 60753: https://problems.ru/view_problem_details_new.php?id=60753

View graph