Formalizing Galois Theory

Thomas Browning, Patrick Lutz

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 curricul…