Department of Computer Science and Technology

Technical reports

A formal proof of Sylow’s theorem
An experiment in abstract algebra with Isabelle Hol

Florian Kammüller, Lawrence C. Paulson

November 1998, 30 pages

DOI: 10.48456/tr-452

Abstract

The theorem of Sylow is proved in Isabelle HOL. We follow the proof by Wielandt that is more general than the original and uses a non-trivial combinatorial identity. The mathematical proof is explained in some detail leading on to the mechanization of group theory and the necessary combinatorics in Isabelle. We present the mechanization of the proof in detail giving reference to theorems contained in an appendix. Some weak points of the experiment with respect to a natural treatment of abstract algebraic reasoning give rise to a discussion of the use of module systems to represent abstract algebra in theorem provers. Drawing from that, we present tentative ideas for further research into a section concept for Isabelle.

Full text

PDF (0.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-452,
  author =	 {Kamm{\"u}ller, Florian and Paulson, Lawrence C.},
  title = 	 {{A formal proof of Sylow's theorem : An experiment in
         	   abstract algebra with Isabelle Hol}},
  year = 	 1998,
  month = 	 nov,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-452.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-452},
  number = 	 {UCAM-CL-TR-452}
}