The Coq mailing list

[Chris Casinghino <chris.casinghino AT gmail.com>]

Hi Coq Club,

Brian Aydemir and I are pleased to announce a completed coq proof
of Fermat's last theorem.  Attached, you'll find the .v file.

It's known to compile with both coq 8.1 and 8.2 using coqc on the
command line.  Note that you won't be able to step through it in proof
general or coqide, though, because it depends on a feature they don't
implement.

--Chris Casinghino

Attachment: fermat.v
Description: Binary data