The goal of this project is to formalize Galois Theory on Isabelle/HOL. As a base for this development the library HOL-Algebra is used. Even if fairly complete as a library of elementary algebra, there are still some fundamental results that are missing in this library. So together with its use, a lot of modifications are being done.
- Clemens Ballarin, who wrote the HOL-Algebra library.
- Larry Paulson, who supervised our work and answered inumerous questions.
- Anthony Bordg, who co-supervised our work and firstly oriented us towards the formalization of Algebra.