R. Apéry, Irrationalité de ?(2) et ?(3) Astérisque, 61, 1979.

F. Besson, Fast Reflexive Arithmetic Tactics the Linear Case and Beyond, TYPES'06, pp.48-62, 2007.
DOI : 10.1007/978-3-540-74464-1_4

F. Beukers, A Note on the Irrationality of ??(2) and ??(3), Bulletin of the London Mathematical Society, vol.11, issue.3, pp.268-272, 1979.
DOI : 10.1112/blms/11.3.268

F. Chyzak, A. Mahboubi, and T. Sibut-pinote, Do creative-telescoping algorithms provide complete proofs? a formal study of Apéry's theorem, 2014.

F. Chyzak and B. Salvy, Non-commutative Elimination in Ore Algebras Proves Multivariate Identities, Journal of Symbolic Computation, vol.26, issue.2, pp.187-227, 1998.
DOI : 10.1006/jsco.1998.0207
URL : https://hal.archives-ouvertes.fr/hal-01069833

C. Cohen, Construction of Real Algebraic Numbers in Coq, ITP, 2012.
DOI : 10.1007/978-3-642-32347-8_6
URL : https://hal.archives-ouvertes.fr/hal-00671809

C. Cohen, Formalized algebraic numbers: construction and first-order theory, 2012.
URL : https://hal.archives-ouvertes.fr/pastel-00780446

C. Cohen, M. Dénès, and A. Mörtberg, Refinements for free! In CPP, LNCS, vol.8307, pp.147-162, 2013.

D. Delahaye and M. Mayero, Dealing with algebraic expressions over a field in Coq using Maple, Journal of Symbolic Computation, vol.39, issue.5, pp.569-592, 2005.
DOI : 10.1016/j.jsc.2004.12.004
URL : https://hal.archives-ouvertes.fr/hal-01125074

B. Feng, An Simple Elementary Proof for the Inequality d n < 3 n, Acta Mathematicae Applicatae Sinica, English Series, vol.29, issue.3, pp.455-458, 2005.
DOI : 10.1007/s10255-005-0252-9

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

D. Hanson, On the product of the primes, Bulletin canadien de math??matiques, vol.15, issue.0, pp.33-37, 1972.
DOI : 10.4153/CMB-1972-007-7

J. Harrison, Formalizing an Analytic Proof of the Prime Number Theorem, Journal of Automated Reasoning, vol.104, issue.1:2, pp.243-261, 2009.
DOI : 10.1007/s10817-009-9145-6

J. Harrison and L. Théry, A skeptic's approach to combining HOL and Maple, Journal of Automated Reasoning, vol.21, issue.3, pp.279-294, 1998.
DOI : 10.1023/A:1006023127567

C. Keller and B. Werner, Importing HOL Light into Coq, ITP, pp.307-322, 2010.
DOI : 10.1007/978-3-642-14052-5_22
URL : https://hal.archives-ouvertes.fr/inria-00520604

A. Mahboubi and B. Gregoire, Proving equalities in a commutative ring done right in Coq, TPHOLs 2005, pp.98-113, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00819484

R. H. Risch, The solution of the problem of integration in finite terms, Bulletin of the American Mathematical Society, vol.76, issue.3, pp.605-608, 1970.
DOI : 10.1090/S0002-9904-1970-12454-5

B. Salvy, An Algolib-aided version of Apéry's proof of the irrationality of ?(3), 2003.

A. Van-der-poorten, Ap??ry???s Proof of the irrationality of ??(3), The Mathematical Intelligencer, vol.1, issue.4, pp.195-203, 1979.
DOI : 10.1007/BF03028234

D. Zeilberger, A holonomic systems approach to special functions identities, Journal of Computational and Applied Mathematics, vol.32, issue.3, pp.321-368, 1990.
DOI : 10.1016/0377-0427(90)90042-X

D. Zeilberger, The method of creative telescoping, Journal of Symbolic Computation, vol.11, issue.3, pp.195-204, 1991.
DOI : 10.1016/S0747-7171(08)80044-2