A New Look at the Fundamental Theorem of Algebra
In this talk we will explore one application of a constructive
formalization of the Fundamental Theorem of Algebra.
We begin by discussing the theoretical and practical interest of
formalizing mathematics, before a constructive proof of the FTA is
presented in detail. Then we look at the algorithm implicit in this
proof to focus on the problem of extracting the corresponding computer
program from a computer representation of the proof.
(Centro de Lógica e Computação, IST, Lisboa)
January 20, 2004