Prove2Me

Solvability of x4+x3+x2+x+1≡0(modp)x^4+x^3+x^2+x+1\equiv 0 \pmod p implies p≡1(mod5)p\equiv 1 \pmod 5; infinitely many primes 5n+15n+1

Proved
AlfutovaUstinov.problem_4_131

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

cyclotomic-polynomialselementary-number-theorynumber-theoryprimes-in-progressions

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

  1. Let p>5p>5 be a prime. If the congruence
x4+x3+x2+x+1≡0(modp)x^{4}+x^{3}+x^{2}+x+1\equiv 0 \pmod p

has an integer solution xx, then p≡1(mod5)p\equiv 1 \pmod 5.

  1. There are infinitely many primes of the form 5n+15n+1, n∈Nn\in\mathbb N (the book asks to deduce this from part 1).

Part 1 describes the prime divisors of values of the cyclotomic polynomial Φ5(x)=x4+x3+x2+x+1\Phi_5(x)=x^4+x^3+x^2+x+1; part 2 is a special case of Dirichlet's theorem on primes in arithmetic progressions.

Formalization Note Part 1 quantifies over natural numbers pp with Nat.Prime p and 5<p5<p, with x∈Zx\in\mathbb Z and the congruence expressed with Int.ModEq; its conclusion uses Nat.ModEq. Part 2 states that the set of primes pp with p=5n+1p=5n+1 for some n∈Nn\in\mathbb N is infinite.

Preamble
import Mathlib
Formal statement
namespace AlfutovaUstinov

theorem problem_4_131 :
    (∀ p : ℕ, p.Prime → 5 < p →
        (∃ x : ℤ, x ^ 4 + x ^ 3 + x ^ 2 + x + 1 ≡ 0 [ZMOD p]) → p ≡ 1 [MOD 5]) ∧
      {p : ℕ | p.Prime ∧ ∃ n : ℕ, p = 5 * n + 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.131. Problem text and answer as catalogued on problems.ru, problem 60757: https://problems.ru/view_problem_details_new.php?id=60757

View graph