Is $257^{1092}+1092$ prime? (No.)

Proved

AlfutovaUstinov.problem_4_120

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

elementary-number-theoryfermat-little-theoremnumber-theoryprimality

This is Problem 4.120 of N. B. Alfutova and A. V. Ustinov, Algebra and Number Theory (MCCME, 2002), Chapter 4, §4 “Theorems of Fermat and Euler”. The problem asks whether the number $257^{1092}+1092$ is prime; the book's answer is that it is not.

Theorem. The natural number

257^{1092}+1092

is not prime.

Like the neighbouring exercises, this illustrates how Fermat's little theorem reveals a divisor of a number far too large to factor by hand.

Formalization Note Primality is Nat.Prime on $\mathbb N$ .

Preamble

import Mathlib

Formal statement

namespace AlfutovaUstinov

theorem problem_4_120 : ¬ Nat.Prime (257 ^ 1092 + 1092) := 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.120. Problem text and answer as catalogued on problems.ru, problem 60746: https://problems.ru/view_problem_details_new.php?id=60746

View graph

Is 2571092+1092257^{1092}+10922571092+1092 prime? (No.)

Is $257^{1092}+1092$ prime? (No.)