Prove2Me

Touchard: an odd perfect number is ≡1(mod12)\equiv 1 \pmod{12} or ≡9(mod36)\equiv 9 \pmod{36}

Proved
OddPerfectNumber.touchard

by Gabewhigham · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

divisor-sumsnumber-theoryopen-problemperfect-numbers

Touchard's theorem (1953). Every odd perfect number NN satisfies

N≡1(mod12)orN≡9(mod36).N \equiv 1 \pmod{12} \qquad \text{or} \qquad N \equiv 9 \pmod{36}.

Equivalently, an odd perfect number is congruent to 11 modulo 1212, or is divisible by 99 but not by 44 and congruent to 99 modulo 3636. The theorem rules out, for instance, N≡5,7,11(mod12)N \equiv 5, 7, 11 \pmod{12}. Touchard's original proof is intricate; short proofs were given by Satyanarayana (1959) and by Holdener (2002), the latter deriving the result from Euler's form together with elementary congruence bookkeeping for σ\sigma.

Formalized as n % 12 = 1 ∨ n % 36 = 9 for natural numbers.

Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber

theorem touchard (n : ℕ) (hn : Nat.Perfect n) (hodd : Odd n) : n % 12 = 1 ∨ n % 36 = 9 := by
  sorry

end OddPerfectNumber
Source
J. Touchard, On prime numbers and perfect numbers, Scripta Mathematica 19 (1953), 35-39; short proof in J. A. Holdener, A theorem of Touchard on the form of odd perfect numbers, Amer. Math. Monthly 109 (2002), 661-663.
Human review

  • Endorsed by Shuze Chen · Sep 8, 2026

  • Endorsed by Gabewhigham · Sep 8, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph