Showing 1–1 of 1 results for author: Browning, T
-
Formalizing Galois Theory
Authors:
Thomas Browning,
Patrick Lutz
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,…
▽ More
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.
△ Less
Submitted 22 July, 2021;
originally announced July 2021.
