The "Fundamental Theorem of Algebra" Project



In the group of Henk Barendregt, a number of people have coded the full proof of a significant mathematical theorem in the computer. The theorem chosen for this project was the "Fundamental Theorem of Algebra" (which states that every non-constant polynomial P over the complex numbers has a "root", i.e., that every non-trivial polynomial equation P(z)=0 always has a solution in the complex plane), and the system used was the Coq system from France.

This page briefly presents the project. Five people have contributed to the coding:

Herman is the person who started the project and who manages it. Apart from Randy, these people all work in Nijmegen. Randy contributed remotely from Edinburgh, keeping contact by e-mail and CVS.

The type theory of Coq naturally corresponds to a constructive logic, so it was decided to translate a constructive proof of the Fundamental Theorem. The proof that was chosen was the so-called "Kneser" proof, which analyzes an iterative proces that converges to one of the roots of the equation.

We decided to treat the real numbers axiomatically, as a "parameter" to the development (because constructive real numbers were needed, the axiomatic real numbers from the Coq distribution weren't usable and an own version of the real number axioms was created). Because of this approach, any representation of the constructive real numbers can be "plugged in" into the proof. Milad Niqui, a Ph.D. student from our group, has created such an "implementation" of the real numbers.

The type theory of Coq is sufficiently powerful that we can prove the theorem without postulating any axioms. (This is not entirely true: because of a technical difficulty with Coq we need one axiom. The technical difficulty is that in Coq a proof of the existence and uniqueness of an object can't be used as a definition of that object.)

The project consisted of three phases:

  1. Writing in LaTeX a detailed account of the Kneser proof in ordinary mathematical style
  2. Writing in Coq the steps of the Kneser proof but as axioms, so without any Coq proofs: a so-called theory development
  3. "Filling in" the Coq proofs in this theory development, leading to a proof development

There are three main "products" of the project:

  • The LaTeX document that gives the proof in natural language (here is the version of 2000-11-11 both as gzipped postscript and as dvi)
  • The Coq version of the proof of the Fundamental Theorem of Algebra (here is the final version of 2000-11-11 as a gzipped tar file: it runs under Coq version 6.3.1)
  • A LaTeX document that documents the Coq proof, which is automatically generated from annotations in the Coq files in the spirit of "literate programming" (here is the version of 2000-11-11 both as gzipped postscript and as dvi)

The Coq proof consists of rather different parts. For instance there are:

  • Basic algebraic structures: groups, rings, fields, ordered fields, etc. (because the development is constructive, it is not based on the customary notion of "Setoids", but instead it is based on "CSetoids" in which "apartness" is the fundamental notion). This all culminates in a Coq type "CReals", which one may think of as a "real number structure" (this is a self-contained extract from the development presenting the definition of the CReals type). In order to "shop" for an implementation of the real numbers, a "flattened", variant of this type called CReals45 has been created too, making the list of axioms of a real number structure more clear.
  • Definitions and basic theory of "elementary" mathematical objects: complex numbers, vector spaces, matrices, polynomials, continuous real functions.
  • "Tools" to do algebraic reasoning. On the one hand there are the "Step" and "Step2" tactics, which use "Auto" to automatically do calculations involving the Setoid equality (instead of Coq's usual Leibniz equality). On the other hand there is "Rational", a tactic that uses the "two-level approach" (often called "reflection") to simplify expressions in a field. The "Rational" tactic generalizes Coq's "Ring" tactic for our algebraic structures, but because expression can become undefined because of division by zero it implements partial reflection (for a description of this, see our TPHOLs paper Equational Reasoning via Partial Reflection.)
  • The "Kneser" proof: this is the "mathematical meat" of the development, the only part that is really about the Fundamental Theorem of Algebra.

(last modification 2000-11-11)