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

[Joe Shipman]

Is there a reverse project, whereby the Formal 40,000 line proof of the Odd Order Theorem can be translated back into a human-readable form that is much more complete and self-contained than the original published OOT proof?

— JS

Sent from my iPhone

> On Jan 15, 2018, at 5:05 AM, Frédéric Blanqui <frederic.blanqui at inria.fr> wrote:
> 
> 
> 
>> Le 12/01/2018 à 14:20, Tennant, Neil a écrit :
>> The blow-up factor from informal to formal proof looks to be two or three orders of magnitude, even for such a
>> simple and informally compelling result as the irrationality of sqrt(2). One shudders to think what the blow-up factor 
>> (for faithful formalization) would be for the current informal proof of FLT!
> 
> Hello. Proof assistants make progress every day and have been improved a lot compared to 20 years ago. The increase factor depends on many things and what is exactly taken into account. For instance, for the formalization of the odd-order theorem, the increase factor was 4 or 5. See https://doi.org/10.1007/978-3-642-39634-2_14 for details. "The roughly 250 pages of mathematics in our two main sources [6, 36] translate to about 40,000 lines of formal proof." Currently, one of the 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.
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180115/6f470103/attachment.html>