[FOM] foundations meeting/FOMUS/discussion

[Mario Carneiro]

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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160326/9dd0dfa4/attachment-0001.html>