[FOM] foundations meeting/FOMUS/discussion

[Josef Urban]

It is similar with Mizar. The Coq proof was much bigger and took much
longer than the Mizar proof. Not (only) because it was constructive,
but (also) because Robert Milewski who did the Mizar proof could use
Mizar's much larger library. For Coq, it looked (to me) like one of
the largest early formalizations in that system - which is always a
test of its technologies. Btw., there are also proofs in Isabelle and
HOL Light. IIRC, Andrzej Trybulec claimed that the proof took only a
couple of days to John Harrison.

Josef

On Sat, Mar 26, 2016 at 10:42 PM, Mario Carneiro <di.gama at gmail.com> wrote:
>
>
> On Sat, Mar 26, 2016 at 1:18 PM, Ben Sherman <sherman at csail.mit.edu> wrote:
>>
>> Looking at Freek Wiedijk's "Formalizing 100 Theorems" page
>> (http://www.cs.ru.nl/~freek/100/), we see a constructive formulation of the
>> Fundamental Theorem of Algebra has been proved in Coq:
>> https://www.cs.ru.nl/~freek/fta/xindex.html
>>
>> http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.77.377&rep=rep1&type=pdf
>>
>> The development is roughly 40,000 lines of Coq code and depends only on
>> the Coq standard library, so it is essentially "from the ground up". HoTT
>> (with propositional resizing) is an extension of Coq, so the proof in Coq
>> also serves as a proof in HoTT.
>>
>> There are also proofs of the Fundamental Theorem of Algebra in Metamath:
>> http://us.metamath.org/mpegif/fta.html
>> as well as Mizar:
>> http://www.mizar.org/JFM/Vol12/polynom5.abs.html
>> which I believe are both based on ZFC.
>>
>> I would doubt that any of these developments required significantly more
>> effort than the others, but can't say for sure.
>
>
> This is probably a highly unfair comparison, but the Metamath proof of the
> FTA was significantly less complicated than the Coq proof. After compression
> (the default for Metamath proofs), the proof is 437 lines (~31000 bytes),
> much less than the quoted ~40000 lines of Coq. However, this only counts the
> "meat" of the proof, not any of the preliminaries for dealing with
> polynomials and real numbers (which are part of the library, although we put
> everything in the library so that's not saying much). It is also not
> constructive, and certainly did not rebuild the whole theory for
> constructive real numbers as the Coq team did.
>
> Make of this data what you will for answering the original question of ZFC
> vs. dependent type theory.
>
> Mario
>
>>
>>
>> Personally, I am currently using Coq to formalize some analysis, and
>> though I am not familiar with constructing formal proofs in ZFC, I do not
>> think there would be any significant difficulty for proving either of these
>> theorems using Coq, and therefore HoTT as well (with propositional
>> resizing).
>>
>> (I assume by "rigorous" you mean formal.)
>>
>> On March 26, 2016, at 12:07 PM, Joe Shipman <joeshipman at aol.com> wrote:
>>
>>
>> Let's make this extremely concrete. I am going to pick two very well-known
>> theorems of different levels of difficulty. Can people who think HoTT is a
>> useful "alternative foundation" for mathematics please say whether or not
>>
>> (1) the Prime Number Theorem can be rigorously proved using foundations
>> involving HoTT and no set theory without significantly more effort than the
>> standard development  requires, counting effort "from the ground up"
>>
>> (2) the Fundamental  Theorem of Algebra can be rigorously proved using
>> foundations involving HoTT and no set theory without significantly more
>> effort than the standard development  requires, counting effort "from the
>> ground up"
>>
>> -- JS
>>
>>
>>
>> _______________________________________________
>> FOM mailing list
>> FOM at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/fom
>>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>