[FOM] foundations meeting/FOMUS/discussion

[Ben Sherman]

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.

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160326/288df90c/attachment-0001.html>