Formalizing Galois Theory: I automorphism groups of fields

Title from first page of PDF file (viewed Dec. 9, 2011)Committee members: Wayne Aitken (chair), K. Brooks Reid, Olaf HansenThesis (M.S.)--California State University San Marcos, 2011Includes bibliographical references (p. 79-81)This thesis focuses on formalizing results involving automorphism groups of fields using the proof assistant Isabelle. Chapter 1 serves as an introduction to the thesis topic and includes a short history of computer proof assistants. In Chapter 2, we included a more detailed description of the proof assistant Isabelle, an example of a formalized proof, and a discussion on formalizing issues. Chapter 3 contains a series of definitions, propositions, and theorems along with their proofs, culminating with a detailed proof of the fundamental theorem of Galois theory. In Chapter 4 we explain the process of formalizing some of the results from Chapter 3, including Isabelle examples. The last chapter contains a summary of the formalized material and reflects on the results from Chapter 3 that remain to be formalized. As an appendix, we also included the Isabelle code containing the formalized lemmas and theorems developed for this thesis and described in Chapter