<abstract xml:lang="en" xmlns="http://www.w3.org/1999/xhtml"><p>This article formalizes proofs of some elementary theorems of number theory (see [1, 26]): Wilson's theorem (that <italic>n</italic> is prime iff <italic>n</italic> > 1 and (<italic>n</italic> - 1)! ≅ -1 (mod <italic>n</italic>)), 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 Σ<sub>k|<italic>n</italic></sub> Φ(<italic>k</italic>) = <italic>n</italic>.</p></abstract>

This article formalizes proofs of some elementary theorems of number theory (see [1, 26]): 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.

The Perfect Number Theorem and Wilson's Theorem

Casella Postale 49, 54038 Montignoso, Italy

Formalized Mathematics

{"article-title":"The Perfect Number Theorem and Wilson's Theorem"}

This article formalizes proofs of some elementary theorems of number theory (see [1, 26]): Wilson's theorem (that n is prime iff n > 1 and (n - 1)! ≅ -1 (mod...

The Perfect Number Theorem and Wilson's Theorem

Published Online: Jul 14, 2009

Page range: 123 - 128

DOI: https://doi.org/10.2478/v10037-009-0013-y

This content is open access.