[FOM] What is the current state of the research about proving FLT?

[revantha]

> reasons why formalizations take a lot of time is the lack of libraries
> providing even basic or more advanced definitions and results in the
> various fields of mathematics. The formalization of the odd-order
> theorem required the development of many libraries on group theory,
> linear algebra, algebraic numbers, Galois theory, etc. that did not
> exist before. Now that they exist, the formalization of new results in
> this field should take less time. Fr?d?ric.
> 

An aside, but something that puzzles me: when formalising e.g. the
odd-order theorem, what is the need (given the cost in time and effort)
to formalise all the well-known results on group theory, linear algebra,
algebraic numbers, Galois theory in the same project? I suppose that it
is nice to formalise everything from scratch, but why undertake this at
the same time as formalising the main theorem?

Is it the concern that if the well-known results are introduced as
"axioms", then some incorrect entry might introduce a false claim?

Best,

Revantha.