Titre:  A constructive proof of the Fundamental Theorem of Algebra in Coq
Résumé:
 

Joint work with Freek Wiedijk and Randy Pollack

In Nijmegen we are working on formalizing a constructive proof of the
Fundamental Theorem of Algebra (FTA) in Coq. The goal of this enterprise
is manyfold. First we want to show that a large theory development
containing some real mathematics can be done. Second we want to gain
experience in setting up and performing such a large project. Third, we
want to investigate how type theory or the specific implementation (Coq)
can be used in an optimal way (or how they should be improved) to
complete our proof development.

In the project we distinguish three phases:
1. Writing the mathematical theory (incl. proofs) on paper,
2. Theory development in Coq: setting up the definitions and stating the
theorems to be proved,
3. Proof development in Coq: proving the theorems.
These phases are not executed sequentially, but in interaction with
oneanother.
At this moment , phase 1 has been finished . We are in the process of
theory development: setting up
the definitions and the theorems to be proved. Some proof development
has been done.

In the talk we shall report on the experience with setting up the
project and how the three different phases interact. Furthermore we
shall discuss some of the specific choices we have made in the
formalization and some of the more interesting mathematical aspects
related to the approach we have chosen.
Also, we will discuss some approaches to reasoning with equalities that
we have tried out.