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

[Frédéric Blanqui]

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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180115/23668de9/attachment-0001.html>