Prove2Me

For a prime p=4k+1p=4k+1, the numbers x=±(2k)!x=\pm(2k)! solve x2+1≡0(modp)x^2+1\equiv 0 \pmod p

Proved
AlfutovaUstinov.problem_4_128

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

elementary-number-theorynumber-theoryquadratic-residueswilson-theorem

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

Theorem. Let pp be a prime of the form p=4k+1p=4k+1 with k∈Nk\in\mathbb N. Then both numbers x=(2k)!x=(2k)! and x=−(2k)!x=-(2k)! are solutions of the congruence

x2+1≡0(modp).x^{2}+1\equiv 0 \pmod p .

This gives an explicit square root of −1-1 modulo every prime p≡1(mod4)p\equiv 1 \pmod 4, complementing Problem 4.126, which shows that no such square root exists for primes p≡3(mod4)p\equiv 3 \pmod 4. It is a consequence of Wilson's theorem.

Formalization Note The factorial is Nat.factorial, cast to Z\mathbb Z; the two claims (for +(2k)!+(2k)! and −(2k)!-(2k)!) are stated separately as congruences in Z\mathbb Z (Int.ModEq).

Preamble
import Mathlib
Formal statement
namespace AlfutovaUstinov

theorem problem_4_128 (p k : ℕ) (hp : p.Prime) (hpk : p = 4 * k + 1) :
    (Nat.factorial (2 * k) : ℤ) ^ 2 + 1 ≡ 0 [ZMOD p] ∧
      (-(Nat.factorial (2 * k) : ℤ)) ^ 2 + 1 ≡ 0 [ZMOD p] := 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.128. Problem text and answer as catalogued on problems.ru, problem 60754: https://problems.ru/view_problem_details_new.php?id=60754

View graph