Abstract
This paper describes a machine-checked proof of the Jordan-Hölder theorem for finite groups. This purpose of this description is to discuss the representation of the elementary concepts of finite group theory inside type theory. The design choices underlying these representations were crucial to the successful formalization of a complete proof of the Odd Order Theorem with the Coq system.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
The Coq Proof Assistant, http://coq.inria.fr
Aschbacher, M.: Finite Group Theory. Cambridge Studies in Advanced Mathematics. Cambridge University Press (2000)
Bender, H., Glauberman, G.: Local analysis for the Odd Order Theorem. London Mathematical Society, LNS, vol. 188. Cambridge University Press (1994)
Bertot, Y., Castéran, P.: Interactive theorem proving and program development: Coq’Art: The calculus of inductive constructions. Springer, Berlin (2004)
Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 86–101. Springer, Heidelberg (2008)
de Bruijn, N.G.: The mathematical language AUTOMATH, its usage, and some of its extensions. In: Laudet, M., Lacombe, D., Nolin, L., Schützenberger, M. (eds.) Symposium on Automatic Demonstration. Lecture Notes in Mathematics, vol. 125, pp. 29–61. Springer, Heidelberg (1970)
Feit, W., Thompson, J.G.: Solvability of groups of odd order. Pacific Journal of Mathematics 13(3), 775–1029 (1963)
Garillot, F.: Generic Proof Tools and Finite Group Theory. PhD thesis, École polytechnique (2011)
Gonthier, G.: Point-free, set-free concrete linear algebra. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 103–118. Springer, Heidelberg (2011)
Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S.L., Mahboubi, A., O’Connor, R., Biha, S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Théry, L.: A machine-checked proof of the odd order theorem. To appear in the Proceedings of the ITP 2013 Conference (2013)
Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. Journal of Formalized Reasoning 3(2), 95–152 (2010)
Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Théry, L.: A Modular Formalisation of Finite Group Theory. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 86–101. Springer, Heidelberg (2007)
Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Rapport de recherche RR-6455, INRIA (2012)
Hedberg, M.: A coherence theorem for Martin-Löf’s type theory. Journal of Functional Programming 8(4), 413–436 (1998)
Hölder, O.: Zurückführung einer beliebigen algebraischen Gleichung auf eine Kette von Gleichungen. Mathematische Annalen 34(1), 26–56 (1889)
Isaacs, I.: Character Theory of Finite Groups. AMS Chelsea Pub. Series (1976)
Jordan, C.: Traité des substitutions et des équations algébriques. Gauthier-Villars, Paris (1870)
Kurzweil, H., Stellmacher, B.: The Theory of Finite Groups: An Introduction. Universitext Series. Springer (2010)
Mahboubi, A., Tassi, E.: Canonical structures for the working coq user. To appear in the Proceedings of the ITP 2013 Conference (2013)
Peterfalvi, T.: Character Theory for the Odd Order Theorem. London Mathematical Society, LNS, vol. 272. Cambridge University Press (2000)
The Univalent Foundations Program. Homotopy type theory: Univalent foundations of mathematics. Technical report, Institute for Advanced Study (2013)
Wiedijk, F.: The “de Bruijn factor”, http://www.cs.ru.nl/~freek/factor/
Zassenhaus, H.: Zum satz von Jordan-Hölder-Schreier. Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg 10(1), 106–108 (1934)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mahboubi, A. (2013). The Rooster and the Butterflies. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds) Intelligent Computer Mathematics. CICM 2013. Lecture Notes in Computer Science(), vol 7961. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39320-4_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-39320-4_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39319-8
Online ISBN: 978-3-642-39320-4
eBook Packages: Computer ScienceComputer Science (R0)