Prove2Me

Solvability of x2+x+1≡0(modp)x^2+x+1\equiv 0 \pmod p implies p≡1(mod6)p\equiv 1 \pmod 6; infinitely many primes 6k+16k+1

Proved
AlfutovaUstinov.problem_4_130

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

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

This is Problem 4.130 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>3p>3 be a prime. If the congruence
x2+x+1≡0(modp)x^{2}+x+1\equiv 0 \pmod p

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

  1. There are infinitely many primes of the form 6k+16k+1, k∈Nk\in\mathbb N (the book asks to deduce this from part 1).

Part 1 describes the primes dividing values of the cyclotomic polynomial Φ3(x)=x2+x+1\Phi_3(x)=x^2+x+1, and 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 3<p3<p, with the solution xx taken in Z\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=6k+1p=6k+1 for some k∈Nk\in\mathbb N is infinite.

Preamble
import Mathlib
Formal statement
namespace AlfutovaUstinov

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

View graph