Formalizing Galois theory

DOI10.1080/10586458.2021.1986176MaRDI QIDQ5094476zbMATH OpenOpenAlexFDO

Authors Thomas Browning, Patrick Lutz

Publication date 3 August 2022

Published in Experimental Mathematics (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2107.10988

zbMATH Keywords

field theoryformal verificationGalois theoryinteractive theorem provingLean

Mathematics Subject Classification ID

Field theory and polynomials (12-XX) Computer science (68-XX)

Recommendations

• Category theory and Galois theory
• A machine-checked proof of the odd order theorem
• A Modular Formalisation of Finite Group Theory
• Reverse mathematics and algebraic field extensions
• An invitation to model-theoretic Galois theory

Cites work

• A machine-checked proof of the odd order theorem
• Automated reasoning. 10th international joint conference, IJCAR 2020, Paris, France, July 1--4, 2020. Proceedings. Part I
• scientific article; zbMATH DE number 7649968 (Why is no real title available?)
• The Lean theorem prover (system description)

Cited in

(7)

• A formalization of Dedekind domains and class groups of global fields
• Reverse mathematics and algebraic field extensions
• scientific article; zbMATH DE number 7699422 (Why is no real title available?)
• Formalising families of -adic Galois representations in Lean 4
• The Galois connection between IntermediateFields\((E,F)\) and subgroups of \(\mathrm{Aut}(E,F)\)
• The fundamental theorem of Galois theory
• N. G. de Bruijn's contribution to the formalization of mathematics

Describes a project that uses

Uses Software

• mathlib
• Lean
• Isabelle/HOL

This page was built for publication: Formalizing Galois theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5094476)