Galois theory is a cornerstone of undergraduate algebra, but its formalization in a proof assistant requires careful design decisions about how to represent field extensions, automorphism groups, and their interactions.

The authors formalize Galois theory in Lean as part of a larger effort to formalize the standard undergraduate mathematics curriculum. The formalization covers the primitive element theorem, the fundamental theorem of Galois theory, and the equivalence of several characterizations of finite degree Galois extensions. The project required decisions about representing splitting fields, intermediate fields, and the Galois correspondence.

The formalization successfully establishes the primitive element theorem, the fundamental theorem of Galois theory (the correspondence between intermediate fields and subgroups of the Galois group), and multiple equivalent characterizations of Galois extensions in Lean.