Bart Kirkels (WvdI, Eindhoven)

To prove the irreducibility of integer polynomials
so called irreducibility criteria exist. A famous example is the criterion by
Eisenstein. In this lecture I will discuss several criteria and their
corresponding certificates. One of these certificates, which combines
factorizations over finite fields, is studied intensively using Galois
theory.
In this way it can be shown for example, that there exists such a certificate for every irreducible polynomial of prime degree. Next I will describe an algorithm that assigns an irreducibility certificate to every irreducible polynomial. This algorithm was implemented in the Computer Algebra System Magma and tested, together with two other algorithms that assign certificates. Irreducibility certificates can be used in combination with Proof Assistants, to facilitate formally proving irreducibility. I will give a short introduction to this area of Computer Mathematics and describe how this proving can be done using the Proof Assistant Coq. My Master's thesis on this subject (and all accompanying program files) can be found online at http://www.math.ru.nl/~bosma/students/kirkels |