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

[Frédéric Blanqui]

Le 15/01/2018 à 20:07, revantha a écrit :
>> 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?
>
This is indeed possible. Another more pragmatical reason is that this 
helps you get the syntactic representation of objects you are interested 
right. There are many different ways of representing the objects you are 
interested in. Some may be more convenient than others, depending on the 
context. Sometimes, it may even be useful to have different 
representations at the same time and switch between them depending on 
the context. As explained by Gonthier et al: "During the formalization, 
we had to correct or rephrase a few arguments in the texts we were 
following, but the most time-consuming part of the project involved 
getting the base and intermediate libraries right. This required 
systematic consolidation phases performed after the production of new 
material."

> Best,
>
> Revantha.
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom