Formalizing Galois theory

DOI10.1080/10586458.2021.1986176OpenAlexW3207437697MaRDI QIDQ5094476FDOQ5094476

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

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

zbMATH Keywords

Galois theoryformal verificationinteractive theorem provingfield theoryLean

Mathematics Subject Classification ID

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

Cites Work

• The Lean theorem prover (system description)
• Automated reasoning. 10th international joint conference, IJCAR 2020, Paris, France, July 1--4, 2020. Proceedings. Part I
• A machine-checked proof of the odd order theorem
• Title not available (Why is that?)

Cited In (5)

• A formalization of Dedekind domains and class groups of global fields
• N. G. de Bruijn's contribution to the formalization of mathematics
• Reverse mathematics and algebraic field extensions
• Title not available (Why is that?)
• Formalising families of \(\ell \)-adic Galois representations in Lean 4

Uses Software

• Isabelle/HOL
• Lean
• mathlib

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)