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

[Frédéric Blanqui]

Hi. The langage used for describing the machine checkable proof of the 
odd-order theorem, ssreflect (which started to be developed for the 
proof of the 4-color theorem), has been designed so as to better 
separate in each deduction step what is important from what is 
boilerplate or purely syntactical. See 
https://hal.inria.fr/inria-00515548 (introduction) and 
https://hal.inria.fr/inria-00258384 (reference manual). But it still 
difficult to read without running it to see what is the state (goal and 
assumptions) of the prover at each step. I'm not aware of any project 
that would try to automatically generate a human readable summary of 
such a proof. 20 years ago, there has been some work on this topic by 
Yann Coscoy. See for instance http://doi.org/10.1007/BFb0014048, 
http://doi.org/10.1007/BFb0052156 and (in French) 
http://www.theses.fr/2000NICE5428. Best regards, Frédéric.


Le 15/01/2018 à 17:52, Joe Shipman a écrit :
> 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 <mailto: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 <mailto:FOM at cs.nyu.edu>
>> https://cs.nyu.edu/mailman/listinfo/fom
>
>
> _______________________________________________
> 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/20180116/2a1585e9/attachment-0001.html>