Résumé:
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.
See this web page for more information.
Retour au sommaire / Back to schedule