G. Almkvist and B. Berndt, Gauss, Landen, Ramanujan, the arithmeticgeometric mean, ellipses, ?, and the Ladies Diary, pp.125-150, 1988.

. Anonymous, Premì ere composition de mathématiques " , concours externe de recrutement de professeurs certifiés, section mathématiques, 1995.

M. Armand, B. Grégoire, A. Spiwack, and L. Théry, Extending Coq with Imperative Features and Its Application to SAT Verification, Interactive Theorem Proving, First International Conference, pp.83-98, 2010.
DOI : 10.1007/978-3-642-14052-5_8
URL : https://hal.archives-ouvertes.fr/inria-00502496

D. Bailey, P. Borwein, and S. Plouffe, On the rapid computation of various polylogarithmic constants, Mathematics of Computation, vol.66, issue.218, pp.903-913, 1997.
DOI : 10.1090/S0025-5718-97-00856-9

Y. Bertot, Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP '15, pp.147-155, 2015.
DOI : 10.1145/321941.321944
URL : https://hal.archives-ouvertes.fr/hal-01074927

Y. Bertot and G. Allais, Views of Pi: definition and computation, Journal of Formalized Reasoning, vol.7, issue.1, pp.105-129, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01074926

Y. Bertot, N. Magaud, and P. Zimmermann, A proof of GMP square root, Journal of Automated Reasoning, vol.29, issue.3/4, pp.225-252, 2002.
DOI : 10.1023/A:1021987403425
URL : https://hal.archives-ouvertes.fr/inria-00101044

Y. Bertot, L. Rideau, and L. Théry, Distant decimals of pi Available at https://www-sop.inria.fr/marelle/distant-decimals-pi, 2017.

F. Besson, Fast Reflexive Arithmetic Tactics the Linear Case and Beyond, Proceedings of the 2006 International Conference on Types for Proofs and Programs, pp.48-62, 2007.
DOI : 10.1007/978-3-540-74464-1_4

M. Boespflug, M. Dénès, and B. Grégoire, Full Reduction at Full Throttle, Certified Programs and Proofs: First International Conference, pp.362-377, 2011.
DOI : 10.1007/3-540-44464-5_13
URL : https://hal.archives-ouvertes.fr/hal-00650940

S. Boldo, C. Lelay, and G. Melquiond, Coquelicot: A User-Friendly Library of Real Analysis for Coq, Mathematics in Computer Science, vol.24, issue.9, pp.41-62, 2015.
DOI : 10.1109/32.713327
URL : https://hal.archives-ouvertes.fr/hal-00860648

S. Boldo and G. Melquiond, Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq, 2011 IEEE 20th Symposium on Computer Arithmetic, pp.243-252, 2011.
DOI : 10.1109/ARITH.2011.40
URL : https://hal.archives-ouvertes.fr/inria-00534854

M. Jonathan, P. B. Borwein, and . Borwein, Pi and the AGM: A Study in the Analytic Number Theory and Computational Complexity, 1987.

R. P. Brent, Fast Multiple-Precision Evaluation of Elementary Functions, Journal of the ACM, vol.23, issue.2, pp.242-251, 1976.
DOI : 10.1145/321941.321944

H. Cartan, Théorie des filtres Comptes Rendus de l, Académie des Sciences, vol.205, pp.595-598, 1937.

C. Cohen, M. Dénès, and A. Mörtberg, Refinements for free! In Certified Programs and Proofs, Third International Conference, pp.147-162, 2013.

L. Cruz-filipe, Constructive Real Analysis: a Type-Theoretical Formalization and Applications, 2004.

M. Dénès, A. Mörtberg, and V. Siles, A refinement-based approach to computational algebra in Coq, Interactive Theorem Proving -Third International Conference, pp.83-98, 2012.

J. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, Programming Languages and Systems: 22nd European Symposium on Programming, ESOP 2013, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

L. Fousse, G. Hanrot, V. Lefèvre, P. Pélissier, and P. Zimmermann, MPFR, ACM Transactions on Mathematical Software, vol.33, issue.2, 2007.
DOI : 10.1145/1236463.1236468
URL : https://hal.archives-ouvertes.fr/inria-00070266

G. Gonthier, Mathematical components Available at http://math-comp. github

B. Gourevitch, The world of Pi Available at http://www, 1999.

B. Grégoire and L. Théry, A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers, Automated Reasoning: Third International Joint Conference, pp.423-437, 2006.
DOI : 10.1007/11814771_36

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

J. Harrison, Formalizing basic complex analysis In From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric, pp.151-165, 2007.

J. Harrison, Pi series in Bailey/Borwein/Plouffe polylogarithmic constants paper, the HOL Light library Available at https://github.com/jrh13, 2010.

J. Harrison, Theorem Proving with the Real Numbers, 2011.
DOI : 10.1007/978-1-4471-1591-5

J. Hölzl, Proving inequalities over reals with computation in Isabelle/HOL, Proceedings of the ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS'09), pp.38-45, 2009.

J. Hölzl, F. Immler, and B. Huffman, Type classes and filters for mathematical analysis in Isabelle/HOL, Interactive Theorem Proving, pp.279-294, 2013.

L. V. King, On the Direct Numerical Calculation of Elliptic Functions and Integrals, 1924.

R. Krebbers and B. Spitters, Type classes for efficient exact real arithmetic in Coq, Logical Methods in Computer Science, vol.9, issue.1, 2011.
DOI : 10.2168/LMCS-9(1:1)2013

X. Leroy, Proving tight bounds on univariate expressions with elementary functions in Coq, Commun. ACM Journal of Automated Reasoning, vol.52, issue.573, pp.107-115187, 2009.

T. Nipkow, M. Wenzel, and L. C. Paulson, Isabelle/HOL: A Proof Assistant for Higher-order Logic, 2002.
DOI : 10.1007/3-540-45949-9

O. Russell and . Connor, Certified exact transcendental real number computation in Coq, Theorem Proving in Higher Order Logics: 21st International Conference, pp.246-261, 2008.

E. Salamin, Computation of ? using arithmetic-geometric mean, Mathematics of Computation, vol.33, issue.135, 1976.

A. Schönhage and V. Strassen, Fast multiplication of large numbers, Computing, vol.150, issue.3-4, pp.281-292, 1971.
DOI : 10.1007/BF02242355

A. Solovyev and T. C. Hales, Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations, NASA Formal Methods: 5th International Symposium, NFM 2013, pp.383-397, 2013.
DOI : 10.1007/978-3-642-38088-4_26