J. Avigad, Type inference in mathematics, Bull. Eur. Assoc. Theor. Comput. Sci. EATCS, vol.106, pp.78-98, 2012.

H. Bender and G. Glauberman, Local Analysis for the Odd Order Theorem, LNS, vol.188, 1994.
DOI : 10.1017/CBO9780511665592

N. Bourbaki, The Architecture of Mathematics, The American Mathematical Monthly, vol.57, issue.4, 1950.
DOI : 10.2307/2305937

T. Chong, Y. K. Leong, A. , and J. Serre, An interview with Jean-Pierre Serre, The Mathematical Intelligencer, vol.8, issue.4, pp.8-13, 1986.
DOI : 10.1007/BF03026112

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, Formal proof|the four-color theorem, Notices Amer, Math. Soc, vol.55, issue.11, pp.1382-1393, 2008.

G. Gonthier, A Machine-Checked Proof of the Odd Order Theorem, Lecture Notes in Comput. Sci, vol.7998, pp.163-179, 2013.
DOI : 10.1007/978-3-642-39634-2_14
URL : https://hal.archives-ouvertes.fr/hal-00816699

C. Thomas and . Hales, A proof of the Kepler conjecture, Ann. of Math, vol.162, issue.23, pp.1065-1185, 2005.

C. Thomas and . Hales, A formal proof of the Kepler conjecture, arxiv.org, 2015.

A. Harald and . Helfgott, The ternary Goldbach conjecture is true, arxiv.org/abs/1312, 2013.

. Yu and . Ilyashenko, Centennial history of Hilbert's 16th problem, Bull. Amer. Math. Soc. (N.S.), vol.39, issue.3, pp.301-354, 2002.

. 14-gerwin-klein, sel4: formal verification of an os kernel, SOPS ACM SIGOPS, pp.207-220, 2009.

X. Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, POPL, pp.42-54, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

T. Peterfalvi, Character Theory for the Odd Order Theorem, LNS, vol.272, 2000.
DOI : 10.1017/CBO9780511565861

R. Solomon, A brief history of the classification of the finite simple groups, Bulletin of the American Mathematical Society, vol.38, issue.03, pp.315-352, 2001.
DOI : 10.1090/S0273-0979-01-00909-0

P. William and . Thurston, On proof and progress in mathematics, Bull. Amer. Math. Soc. (N.S.), vol.30, issue.2, pp.161-177, 1994.

T. 21-warwick, The Lorenz attractor exists, Comptes Rendus de l, Academie des Sciences, Series I ? Mathematics, vol.328, issue.12, pp.1197-1202, 1999.

C. Villani, Birth of a Theorem: A Mathematical Adventure, 2015.