[FOM] blow-up factor

[Dustin Wehr]

Frédéric,
I have often heard what you said about the reasons for long efforts
being the lack of existing libraries. 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?

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