Journal Entry (Sat 14 2024)

A formal proof of Fermat's Little Theorem

Fermat's Little Theorem states that

For all integers $a$, if we have a prime $p$, then $a \bmod p = a^p \bmod p$.

In the accompanying .v file, a formal proof of FLT in the case where $a$ is an integer is provided.

Proof Sketch

The proof formalised here is essentially the same as the one given by Leonard Euler in the 1730s.

First we proceed by induction on a. The base case is trivial.

For the inductive case, we use the idea that when we exponentiate by a prime, all the binomial coefficients except for the last one are a multiple of p and are thus equal to $0$ modulo $p$. (This part of the proof will be referred to as the "Freshman's dream").

The final coefficient will be $1$ and we will have $a^p$, and the inductive hypothesis is applied along with a slew of properties of modular arithmetic to complete the proof.

The sketch itself is formalised as such:

Theorem fermats_little_theorem :
  forall a n: nat,
    (prime n) ->
      a^n mod n = a mod n.

Proof.
  intros a.
  induction a.

  * intros n H_prime.
    destruct H_prime as [H_gt_1 H_divisors].
    rewrite -> Nat.pow_0_l.
    reflexivity.

    {
      rewrite -> Nat.neq_0_lt_0.
      rewrite -> Nat.lt_0_1.
      compute in H_gt_1.
      compute.
      exact H_gt_1.
    }
   
  * intros n H_prime.
    rewrite <- Nat.add_1_r.
    rewrite -> (freshmans_dream a 1 n H_prime).
    rewrite -> Nat.pow_1_l.
    rewrite -> Nat.Div0.add_mod.
    rewrite -> (IHa n H_prime).
    destruct H_prime as [H_gt_1 H_divisors].
    rewrite -> (Nat.mod_1_l n H_gt_1).
    rewrite -> Nat.Div0.add_mod_idemp_l.
    reflexivity.
Qed.    

The freshman's dream here is an assumption used without proof. So let's zoom into it:

Lemma freshmans_dream :
  forall a b p : nat,
    (prime p) ->
    (a + b)^p mod p =
    (a^p + b^p) mod p.

Now the freshman's dream is proved by writing:

Lemma freshmans_dream :
  forall a b p : nat,
    (prime p) ->
    (a + b)^p mod p =
    (a^p + b^p) mod p.

Proof.
  intros a b p H_prime.
  
  destruct (freshmans_awakening a b p H_prime) as [k H_expansion].

  rewrite -> H_expansion.
  Search (_*_ mod _ =_).
  Search (_ + _ mod _).
  rewrite -> (Nat.add_comm).
  rewrite -> (Nat.add_assoc).
  rewrite <- Nat.Div0.add_mod_idemp_r.
  rewrite -> Nat.Div0.mod_mul.
  Search (_ + 0 = _).
  rewrite -> Nat.add_0_r.
  rewrite -> (Nat.add_comm).
  reflexivity.
Qed. 

TODO: Discuss Freshman's awakening.