R. 1. Gonthier and G. , Formal proof -The Four-Color Theorem, Notices of the American Mathematical Society, vol.55, issue.11, 2008.

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, p.509025, 2005.
DOI : 10.1145/1297658.1297660

W. Stephen, The Mathematica Book, Fifth Edition, 2003.

G. The and . Group, GAP ? Groups, Algorithms, and Programming, Version 4.4.12, 2008.

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

G. Gonthier and A. Mahboubi, A small scale reflection extension for the Coq system
URL : https://hal.archives-ouvertes.fr/inria-00258384

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, Coq'Art: the Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

S. Gelbart, An elementary introduction to the Langlands program, Bulletin of the American Mathematical Society, vol.10, issue.2, 1984.
DOI : 10.1090/S0273-0979-1984-15237-6

I. M. Isaacs, Character Theory of Finite Groups, 1994.
DOI : 10.1090/chel/359

G. James and M. Liebeck, Representations and Characters of Groups, 2001.

P. Webb, Finite Group Representations for the Pure Mathematician. The manuscript of the book is available on the author web page http

G. Gonthier, A. Mahboubi, L. Rideau, E. Tassi, and L. Théry, A Modular Formalisation of Finite Group Theory, Theorem Proving in Higher-Order Logics, pp.86-101, 2007.
DOI : 10.1007/978-3-540-74591-4_8
URL : https://hal.archives-ouvertes.fr/inria-00139131

Y. Bertot, G. Gonthier, S. O. Biha, and I. Pasca, Canonical Big Operators, Theorem Proving in Higher-Order Logics, pp.86-101, 2008.
DOI : 10.1007/3-540-44659-1_29
URL : https://hal.archives-ouvertes.fr/inria-00331193

R. Pollack, Dependently Typed Records for Representing Mathematical Structure, Theorem Proving in Higher Order Logics, pp.462-479, 2000.
DOI : 10.1007/3-540-44659-1_29

H. Geuvers, R. Pollack, F. Wiedijk, and J. Zwanenburg, A Constructive Algebraic Hierarchy in Coq, Journal of Symbolic Computation, vol.34, issue.4, pp.271-286, 2002.
DOI : 10.1006/jsco.2002.0552

L. Pottier, User contributions in Coq, Algebra, 1999.

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