Formalizing Galois Theory

TL;DR

This paper details the formalization of core Galois theory results within the Lean theorem prover, contributing to the broader goal of formalizing undergraduate mathematics.

Contribution

It introduces the formalization of key Galois theory theorems in Lean, highlighting challenges and decisions in formalizing advanced algebraic concepts.

Findings

Formalized the primitive element theorem

Formalized the fundamental theorem of Galois theory

Established equivalences of characterizations of Galois extensions

Abstract

We describe a project to formalize Galois theory using the Lean theorem prover, which is part of a larger effort to formalize all of the standard undergraduate mathematics curriculum in Lean. We discuss some of the challenges we faced and the decisions we made in the course of this project. The main theorems we formalized are the primitive element theorem, the fundamental theorem of Galois theory, and the equivalence of several characterizations of finite degree Galois extensions.