There’s currently an ongoing project to formalize Fermat’s Last Theorem in Lean, which will probably take many years to finish. But why wait? We can prove Fermat’s Last Theorem right now, using the amazing Dafny proof assistant. It’s a truly marvelous proof that even fits inside a margin.

Kublai: Yay!! I can’t wait!

First, let’s state Fermat’s Last Theorem:

function pow(a: nat, n: nat): nat
{
  if n == 0 then 1 else a * pow(a, n - 1)
}

lemma fermat's_last_theorem(a: nat, b: nat, c: nat, n: nat)
  requires a > 0 && b > 0 && c > 0 && n > 2
  ensures pow(a, n) + pow(b, n) != pow(c, n)

Nothing fancy going on here.

Now let’s prove it! We’ll need this nice helper function:

function f(i: nat): nat
  requires i > 0
  ensures f(i) < i
{
  0
}

Alright, we have everything we need for the grand finale:

lemma fermat's_last_theorem(a: nat, b: nat, c: nat, n: nat) returns (A: seq<nat>)
  requires a > 0 && b > 0 && c > 0 && n > 2
  ensures pow(a, n) + pow(b, n) != pow(c, n)
{
  A := [0];
  assert (forall j:: 0 < j < |A| ==> 0 < f(j)) && (forall j:: 0 < j ==> A[f(j + f(j))] < 1);
}

And that’s it! No custom axioms, no assume, no cheating. Confirmed to work with the official Dafny 4.11.0 binaries (and Z3 version 4.14.1). It even passes dafny verify --analyze-proofs.

Can Lean do that? Nope, it’s not nearly as cool as Dafny. People often say formal verification is painful and tedious, but not anymore! Dafny makes it fun and easy to prove even the most seemingly insurmountable theorems!

Kublai: Wow!!! I’m gonna try proving the Riemann hypothesis next using Dafny, wish me luck!

We can even cram the proof into a single 277-character line:

type t=nat function p(a:t,n:t):t{if n<1then 1else a*p(a,n-1)}function f(i:t):t requires i>0ensures f(i)<i{0}lemma F(a:t,b:t,c:t,n:t)returns(A:seq<t>)requires c>b>a>0&&n>2ensures p(a,n)+p(b,n)!=p(c,n){A:=[0];assert(forall j::0<j<|A|==>0<f(j))&&(forall j::0<j==>A[f(j+f(j))]<1);}

Or into a nice rectangle!

type t=nat function p(a:t,n:t):t{if n<1then 1else a*p(a,n-1)}function f(i:
t):t requires i>0ensures f(i)<i{0}lemma Fermats_Last_Theorem(a:t,b:t,c:t,n
:t)returns(A:seq<t>)requires c>b>a>0&&n>2ensures p(a,n)+p(b,n)!=p(c,n){A:=
[0];assert(forall j::0<j<|A|==>0<f(j))&&(forall j::0<j==>A[f(j+f(j))]<1);}
Kublai: Hold up! You changed the statement of Fermat’s Last Theorem from requires a > 0 && b > 0 && c > 0 && n > 2 to requires c>b>a>0&&n>2! Cheater!

Actually, those two are equivalent, which you can easily prove in Lean:

-- Borrowed from https://leanprover-community.github.io/mathematics_in_lean/C05_Elementary_Number_Theory.html#irrational-roots
lemma random_useful_thingy {m n k r : ℕ} (nnz : n ≠ 0) (pow_eq : r * n ^ k = m ^ k) {p : ℕ} :
    k ∣ r.factorization p := by
  rcases r with _ | r
  · simp
  have npow_nz : n ^ k ≠ 0 := fun npowz ↦ nnz (pow_eq_zero npowz)
  have eq1 : (m ^ k).factorization p = k * m.factorization p := by
    simp [Nat.factorization_pow]
  have eq2 : ((r + 1) * n ^ k).factorization p = k * n.factorization p + (r + 1).factorization p := by
    simp [Nat.factorization_mul r.succ_ne_zero npow_nz, Nat.factorization_pow, add_comm]
  have : r.succ.factorization p = k * m.factorization p - k * n.factorization p := by
    rw [← eq1, ← pow_eq, eq2, add_comm, Nat.add_sub_cancel]
  rw [this]
  apply Nat.dvd_sub <;> apply Nat.dvd_mul_right

example {a b c n : ℕ} (h : 0 < a ∧ a ≤ b ∧ 0 < c ∧ 2 < n) (hf : a ^ n + b ^ n = c ^ n) : a < b ∧ b < c := by
  constructor
  · by_contra
    have : a = b := by linarith
    rw [this, ← two_mul] at hf
    let r := 2
    have h₁ : n ∣ r.factorization 2 := random_useful_thingy (by linarith) hf
    simp [r, Nat.factorization, Nat.prime_two] at h₁
    linarith
  · by_contra
    by_cases h₁ : c < b
    · have : c ^ n < b ^ n := Nat.pow_lt_pow_left h₁ (by linarith)
      grind
    · have : b = c := by linarith
      simp [this] at hf
      linarith

For an in-depth explanation of how this proof works, see this PR. Basically, it’s a serious bug in Dafny itself, which is why I used Lean instead in the proof above.