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 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 FermatsLastTheorem(a:t,b:t,c:t,n:t
)returns(A:seq<t>)requires c>=b>=a>0&&n>1ensures 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);}

For an in-depth explanation of how this proof works, see this PR.