Prove2Me

Solving φ(x)=2\varphi(x)=2, φ(x)=8\varphi(x)=8, φ(x)=12\varphi(x)=12 and φ(x)=14\varphi(x)=14

Proved
AlfutovaUstinov.problem_4_139

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

diophantine-equationselementary-number-theoryeuler-totientnumber-theory

This is Problem 4.139 of N. B. Alfutova and A. V. Ustinov, Algebra and Number Theory (MCCME, 2002), Chapter 4, §4 “Theorems of Fermat and Euler”. Here φ\varphi denotes Euler's function: φ(x)\varphi(x) is the number of integers among 1,2,…,x1,2,\dots,x coprime to xx. The problem asks to solve the equations (a) φ(x)=2\varphi(x)=2; (b) φ(x)=8\varphi(x)=8; (c) φ(x)=12\varphi(x)=12; (d) φ(x)=14\varphi(x)=14 in natural numbers xx. The book's answers are recorded below.

Theorem. The complete sets of natural solutions are

  1. φ(x)=2  ⟺  x∈{3, 4, 6}\varphi(x)=2 \iff x\in\{3,\,4,\,6\};
  2. φ(x)=8  ⟺  x∈{15, 16, 20, 24, 30}\varphi(x)=8 \iff x\in\{15,\,16,\,20,\,24,\,30\};
  3. φ(x)=12  ⟺  x∈{13, 21, 26, 28, 36, 42}\varphi(x)=12 \iff x\in\{13,\,21,\,26,\,28,\,36,\,42\};
φ(x)=14  has no solutions.\varphi(x)=14 \ \text{ has no solutions.}

Part 4 shows that 1414 is a nontotient: an even number that is not a value of Euler's function.

Formalization Note Euler's function is Nat.totient; each part is stated as an equality of subsets of N\mathbb N. Mathlib's convention φ(0)=0\varphi(0)=0 means that x=0x=0 never solves these equations, so quantifying over all of N\mathbb N agrees with the book's natural numbers x≥1x\ge1.

Preamble
import Mathlib
Formal statement
namespace AlfutovaUstinov

theorem problem_4_139 :
    {x : ℕ | Nat.totient x = 2} = {3, 4, 6} ∧
      {x : ℕ | Nat.totient x = 8} = {15, 16, 20, 24, 30} ∧
      {x : ℕ | Nat.totient x = 12} = {13, 21, 26, 28, 36, 42} ∧
      {x : ℕ | Nat.totient x = 14} = ∅ := 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.139. Problem text and answer as catalogued on problems.ru, problem 60765: https://problems.ru/view_problem_details_new.php?id=60765

View graph