[FOM] blow-up factor

[Frédéric Blanqui]

Le 15/01/2018 à 18:02, Dustin Wehr a écrit :
> Frédéric,
> I have often heard what you said about the reasons for long efforts
> being the lack of existing libraries.
Note that I didn't say that it was the only reason or the main one 
either, but this is an important one.

>   But from the standpoint of the
> current discussion --formalizing controversial proofs for the sake of
> resolving the controversy-- writing formal libraries, or generally
> formally proving any lemmas that are much more obvious than the main
> result (i.e. those which would be clearly asserted but not proved in
> the paper proving the main result), is just perfectionism (provided
> the proof assistant's language lets them be stated in a very clear
> way, of course). Do the often-mentioned 2-4x "blow-up factors" include
> the proofs of such lemmas?
The data I have mentioned are taken from Gonthier & all's paper. They 
correspond to the following books only:

Bender-Glauberman [6] is a book of 174 pages. It translates to 20953 lines.

Peterfalvi [36] is a book of 154 pages. It translates to 19741 lines.

So, this does not include the "more obvious" results that you mention.

Please find more detailed statistics about the whole formalization on 
http://coqfinitgroup.gforge.inria.fr/stat.html .

The statement of the theorem is available here : 
http://coqfinitgroup.gforge.inria.fr/doc/stripped_odd_order_theorem.html 
. It provides the definitions and theorems but not the proof scripts. To 
see the proof scripts, you need to download the Coq files.

Frédéric.

> James,
> Regarding Hales, counting the savings in proof length/complexity that
> come from big efforts in "math land" in favour of proof assistants
> seems like a hard to justify bias in favour of proof assistants.
>
> Everyone,
> If you care about formalization of results, put your (your funders')
> money where your mouth is! There is usually insufficient
> career/reputation reward for formalizing results. That certainly seems
> to be the case for FLT. In other fields, like software engineering
> with "bug bounties", they make up that incentives problem with money
> rewards.
>
>
>> ---------- Forwarded message ----------
>> From: "Frédéric Blanqui" <frederic.blanqui at inria.fr>
>> To: fom at cs.nyu.edu
>> Cc:
>> Bcc:
>> Date: Mon, 15 Jan 2018 11:05:22 +0100
>> Subject: Re: [FOM] What is the current state of the research about proving FLT?
>>
>>
>>
>> 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.
>>
>> ---------- Forwarded message ----------
>> From: James Smith <jecs at imperial.ac.uk>
>> To: Foundations of Mathematics <fom at cs.nyu.edu>
>> Cc:
>> Bcc:
>> Date: Sat, 13 Jan 2018 20:24:23 +0000
>> Subject: Re: [FOM] What is the current state of the research about proving FLT?
>> Hi,
>>
>> On 12/01/18 13:20, Tennant, Neil wrote:
>>> 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!
>>>
>>> So much for "structurally homologous" formalizations of informal proofs.
>> This is a misunderstanding and often the complete opposite is true. Formalised proofs can be "orders and magnitude" simpler and more structured. See here...
>>
>> https://mathoverflow.net/a/281884/93609
>>
>> ...and the link again:
>>
>> [Prof. Thomas Hales - Lessons learned from the Formal Proof of the Kepler Conjecture](https://www.youtube.com/watch?v=Is_lycvOkTA)
>>
>> I feel that it's important that more mathematicians accept this state of affairs rather than deny it.
>>
>> Personally I feel that when proof assistants become more useable, making the work of Hales and others more accessible to mainstream mathematicians, debates such as this one will be a thing of the past. I long for that day...
>>
>> Regards,
>>
>> James
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom