Towards formalization of Fermat's Last Theorem

[mario chiari]

Dear Freek, FOM,  


although I have a very cursory understanding of Formalization of
Mathematics and its challenges, I am very intrigued and curious about
it, and I wish to ask you a couple of very simple minded questions:

-- could it be considered sensible or not  to develop a formalized
version of PA, or maybe better of any one the big five (RCA_0,
WKL_0,..), or maybe of some kind of a common framework for all of them
(and such that it is kept trace of what is proved thanks to what)?

-- is out there any project to develop a on-line, distributed
repository of proofs, such that (authorized?) people may add new
theorems and proofs? 

--  how difficult is to formalize the process of successive
definitional extensions and derived inference rules? (My guess is that
you need quite a lot of them to output something human readable). 

thanks, cheers
mario 

On Mon, 2022-01-10 at 11:25 +0100, Freek Wiedijk wrote:
> 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