The Perfect Number Theorem and Wilson’s Theorem

Summary. This article formalizes proofs of some elementary theorems of number theory (see [26, 1]): Wilson’s theorem (that n is prime iff n> 1 and (n − 1)! ∼ = −1 (mod n)), that all primes (1 mod 4) equal the sum of two squares, and two basic theorems of Euclid and Euler about perfect numbers. The article also formally defines Euler’s sum of divisors function φ, proves that φ is multiplicative and that?k|nφ(k) = n