R. Arthan, Some group theory Available at http://www.lemma-one

J. Avigad, K. Donnelly, D. Gray, and P. Raff, A formally verified proof of the prime number theorem, ACM Transactions on Computational Logic, vol.9, issue.1
DOI : 10.1145/1297658.1297660

G. Barthe, V. Capretta, and O. Pons, Setoids in type theory, Journal of Functional Programming, vol.13, issue.02, pp.261-293, 2003.
DOI : 10.1017/S0956796802004501

URL : https://hal.archives-ouvertes.fr/hal-01124972

H. Bender and G. Glauberman, Local analysis for the Odd Order Theorem. Number 188 in London Mathematical Society Lecture Note Series, 1994.

M. Gregory and . Constantine, Group Theory

W. Feit and J. G. Thompson, Chapter I, from Solvability of groups of odd order, Pacific J. Math, vol. 13, no. 3 (1963, Pacific Journal of Mathematics, vol.13, issue.3, pp.775-1029, 1963.
DOI : 10.2140/pjm.1963.13.775

H. Geuvers, F. Wiedijk, and J. Zwanenburg, A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals, Types for Proofs and Programs, TYPES 2000 International Workshop, pp.96-111, 2002.
DOI : 10.1007/3-540-45842-5_7

G. Gonthier, A computer-checked proof of the four-colour theorem

G. Gonthier, Notations of the four colour thorem proof

J. C. Michael, T. F. Gordon, and . Melham, Introduction to HOL : a theorem proving environment for higher-order logic, 1993.

E. Gunter, Doing Algebra in Simple Type Theory, 1989.

F. Kammüller and L. C. Paulson, A Formal Proof of Sylow's Theorem, Journal of Automated Reasoning, vol.23, issue.3, pp.235-264, 1999.
DOI : 10.1023/A:1006269330992

. Habilitationàhabilitation, Habilitationà diriger les recherches, 1996.

C. Lawrence and . Paulson, Isabelle: a generic theorem prover, LNCS, vol.828, 1994.

T. Peterfalvi, Character Theory for the Odd Order Theorem. Number 272 in London Mathematical Society Lecture Note Series, 2000.

L. Rideau and L. Théry, Formalising Sylow's theorems in Coq, 2006.

B. Werner, Une théorie des Constructions Inductives, 1994.

H. Wielandt, Ein Beweis f???r die Existenz der Sylowgruppen, Archiv der Mathematik, vol.10, issue.1, pp.401-402, 1959.
DOI : 10.1007/BF01240818

Y. Yu, Computer proofs in Group Theory, Journal of Automated Reasoning, vol.6, issue.3, pp.251-286, 1990.
DOI : 10.1007/BF00244488

I. Unité-de-recherche, . Lorraine, . Loria, and . Technopôle-de-nancy, Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-lès-Nancy Cedex (France) Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu -35042 Rennes Cedex (France) Unité de recherche INRIA Rhône-Alpes : 655, avenue de l'Europe -38334 Montbonnot Saint-Ismier (France) Unité de recherche INRIA Rocquencourt, Domaine de Voluceau -Rocquencourt -BP 105 -78153 Le Chesnay Cedex (France) Unité de recherche INRIA Sophia Antipolis : 2004, route des Lucioles -BP 93 -06902 Sophia Antipolis Cedex

I. De-voluceau-rocquencourt, BP 105 -78153 Le Chesnay Cedex (France) http://www.inria.fr ISSN, pp.249-6399