Number theory

Wilson’s theorem: small primes

Compute (p−1)! modulo p and recognize the residue −1.

-- Top 100 #51: Wilson’s theorem: small primes
-- History: 1773 · Lagrange, as dated in the list.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: For a prime p, the nonzero residues pair with their multiplicative inverses.
-- Scope: Verifies the congruence at 5, 7, and 11, plus its failure at composite 8. No primality characterization for arbitrary numbers is proved.
-- Source: https://lurch.plus/100/

def factorial : Nat → Nat
  | 0 => 1
  | n+1 => (n+1) * factorial n

example : (factorial 4 + 1) % 5 = 0 := by decide
example : (factorial 6 + 1) % 7 = 0 := by decide
example : (factorial 10 + 1) % 11 = 0 := by decide
example : (factorial 7 + 1) % 8 ≠ 0 := by decide

#eval factorial 6 % 7

Explanation

`theorem / example`

A named theorem or anonymous example states exactly the claim Lean must check. Read its inputs and assumptions to see the scope.

`decide`

Builds a proof using a decision procedure. Here it checks a concrete arithmetic statement.

`Nat`

Nat contains arbitrary-size natural numbers, including zero. Its subtraction stops at zero.

Background and proof scope

1773 · Lagrange, as dated in the list

For a prime p, the nonzero residues pair with their multiplicative inverses.

Verifies the congruence at 5, 7, and 11, plus its failure at composite 8. No primality characterization for arbitrary numbers is proved.

Historical Top 100 list (reproduced by Lurch)

Expected output

Reference only. Run the file to check its actual result.

Exercise

Try p=13, then p=9. Why does pairing inverses behave differently?