Towards formalization of Fermat's Last Theorem

[Freek Wiedijk]

Dear all,

Formalization of a proof of Fermat's Last Theorem is one of
the Grand Challenges of formalization of mathematics.  We are
considering what is the best way to get started on this.
In particular we currently created a project for this, see

  https://www.cs.ru.nl/~freek/fltfps/

The idea of this project is _not_ to start by formalizing
proofs, but first to formalize _definitions_ and high level
_statements,_ both to show the mathematical communicty what
formalized mathematics looks like, and to create a road
map for a full formalization.  The approach is similar to
the one of Tom Hales' Formal Abstracts project.

My question: does this sound reasonable, or will a different
approach be better?

Freek