Formalizing Galois Theory

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.

KEYWORDS:

• Lean
• interactive theorem proving
• formal verification
• field theory
• Galois theory

6. Acknowledgments

We would like to thank everyone in the Lean community who helped us to complete this project by answering our questions on the Lean Zulip chat and giving us feedback on our pull requests. Special thanks are due to Anne Baanen and Johan Commelin for numerous suggestions, to Kevin Buzzard for helping solve a few technical problems and to Kenny Lau and Anne Baanen for developing a lot of the field theory in $\mathsf{mathlib}$ on which our project depended. We would also like to thank Johan Commelin, Kevin Buzzard and the anonymous referee for reading this article carefully and making many helpful suggestions which greatly improved our exposition. And finally, thanks to all the participants in the Berkeley Lean Seminar during Summer 2020, and especially to Kyle Miller and Jordan Brown.

Declaration of Interest

No potential conflict of interest was reported by the author(s).