J. Abdeljaoued and H. Lombardi, Méthodes matricielles -Introductionàtroduction`troductionà la complexité algébrique, Mathématiques et Applications, 2003.

Z. Ahmed, Ahmed's integral: the maiden solution, Mathematical Spectrum, vol.48, issue.1, pp.11-12, 2015.

K. Appel and W. Haken, Every planar map is four colorable . part i: Discharging, Illinois Journal of Mathematics, vol.21, issue.3, pp.429-490, 1977.

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

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, 2007.
DOI : 10.1145/1297658.1297660

H. Barendregt and E. Barendsen, Autarkic computations in formal proofs, Journal of Automated Reasoning, vol.28, issue.3, pp.321-336, 2002.
DOI : 10.1023/A:1015761529444

H. Barendregt, M. Arjeh, and . Cohen, Electronic Communication of Mathematics and the Interaction of Computer Algebra Systems and Proof Assistants, Journal of Symbolic Computation, vol.32, issue.1-2, pp.3-22, 2001.
DOI : 10.1006/jsco.2001.0455

G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt et al., EasyCrypt: A Tutorial, Foundations of Security Analysis and Design VII, pp.146-166, 2014.
DOI : 10.1145/1594834.1480894

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

F. Bergeron and S. Plouffe, Computing the Generating Function of a Series Given Its First Few Terms, Experimental Mathematics, vol.25, issue.4, pp.307-312, 1992.
DOI : 10.1145/178365.178368

S. Bernard, Y. Bertot, L. Rideau, and P. Strub, Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, 1512.
DOI : 10.1023/A:1026518331905

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

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

K. Bhargavan, A. Delignat-lavaud, C. Fournet, A. Gollamudi, G. Gonthier et al., Thomas Sibut-Pinote, Nikhil Swamy, and Santiago Zanella-Béguelin. Formal Verification of Smart Contracts: Short Paper, In ACM Workshop on Programming Languages and Analysis for Security, 2016.

J. Bingham, Formalizing a proof that e is transcendental, Journal of Formalized Reasoning, vol.4, issue.1, pp.71-84, 2011.

D. Bini, M. Capovani, F. Romani, and G. Lotti, O(n2.7799) complexity for n ?? n approximate matrix multiplication, Information Processing Letters, vol.8, issue.5, pp.234-235, 1979.
DOI : 10.1016/0020-0190(79)90113-3

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

M. Boespflug, M. Dénès, and B. Grégoire, Full Reduction at Full Throttle, Certified Programs and Proofs, Certified Programs and Proofs, 2011.
DOI : 10.1007/3-540-44464-5_13

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

S. Boldo, F. Clément, J. Filliâtre, M. Mayero, G. Melquiond et al., Formal Proof of a Wave Equation Resolution Scheme: The Method Error, Proceedings of the first Interactive Theorem Proving Conference (ITP), pp.147-162, 2010.
DOI : 10.1007/978-3-642-14052-5_12

URL : https://hal.archives-ouvertes.fr/inria-00450789

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

N. Bourbaki, Eléments de mathématique : Livre III. Topologie générale, 1968.

P. Bürgisser, M. Clausen, and A. Shokrollahi, Algebraic complexity theory, 2013.
DOI : 10.1007/978-3-662-03338-8

H. Cartan, Filtres et ultrafiltres Comptes Rendus Hebdomadaires des Séances de l'Académie des Sciences, pp.777-779, 1937.

S. Chevillard, M. Jolde¸sjolde¸s, and C. Lauter, Sollya: An Environment for the Development of Numerical Codes, Mathematical Software - ICMS 2010, pp.28-31, 2010.
DOI : 10.1007/978-3-642-15582-6_5

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

F. Chyzak, A. Mahboubi, T. Sibut-pinote, and E. Tassi, A Computer-Algebra-Based Formal Proof of the Irrationality of ?(3), ITP -5th International Conference on Interactive Theorem Proving, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00984057

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
URL : https://hal.archives-ouvertes.fr/pastel-00780446

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

C. Cohen and A. Mahboubi, Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination, Logical Methods in Computer Science, vol.8, issue.1, pp.21-40, 2012.
URL : https://hal.archives-ouvertes.fr/inria-00593738

H. Cohen, Démonstration de l'irrationalité de ? (3)(d'apres apéry)

D. Coppersmith and S. Winograd, Matrix multiplication via arithmetic progressions, Proceedings of the nineteenth annual ACM symposium on Theory of computing, pp.1-6, 1987.
DOI : 10.1145/28395.28396

F. George and L. B. Corliss, Adaptive, self-validating numerical quadrature, SIAM Journal on Scientific and Statistical Computing, vol.8, issue.5, pp.831-847, 1987.

L. Cruz-filipe, H. Geuvers, and F. Wiedijk, C-CoRN, the Constructive Coq Repository at Nijmegen, Mathematical Knowledge Management, pp.88-103, 2004.
DOI : 10.1007/3-540-45620-1_12

URL : http://repository.ubn.ru.nl/bitstream/2066/104039/1/104039.pdf

J. Philip, P. Davis, and . Rabinowitz, Chapter 4 -error analysis, Methods of Numerical Integration, pp.271-343, 1984.

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

J. Dumas and V. Pan, Fast matrix multiplication and symbolic computation. CoRR, abs, 1612.
URL : https://hal.archives-ouvertes.fr/hal-01417524

J. W. Eaton, D. Bateman, S. Hauberg, and R. Wehbring, GNU Octave version 3.8.1 manual: a high-level interactive language for numerical computations, 2014.

B. Ekici, G. Katz, C. Keller, A. Mebsout, A. J. Reynolds et al., Extending smtcoq, a certified checker for smt, 2016.
DOI : 10.4204/eptcs.210.5

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

L. Euler, Observations on a certain theorem of Fermat and on others concerning prime numbers. ArXiv Mathematics e-prints, 2005.

. Bei-ye-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.4153/CMB-1972-007-7

R. Stéphane-fischler-apéry, Irrationalité de valeurs de zêta (d'après, Séminaire Bourbaki Exposés 909?923, pp.27-62, 2002.

L. Fousse, Intégration numérique avec erreur bornée en précision arbitraire, 2006.

J. Fürlinger and J. Hofbauer, q-Catalan numbers, Journal of Combinatorial Theory, Series A, vol.40, issue.2, pp.248-264, 1985.
DOI : 10.1016/0097-3165(85)90089-5

A. Juan, A. Garay, N. Kiayias, and . Leonardos, The bitcoin backbone protocol: Analysis and applications, EUROCRYPT, pp.281-310, 2015.

R. Michael, . Garey, S. David, and . Johnson, Computers and intractability, wh freeman, vol.29, 2002.

G. Gonthier, The Four Colour Theorem: Engineering of a Formal Proof, Computer Mathematics, pp.333-333, 2008.
DOI : 10.1007/978-3-540-87827-8_28

G. Gonthier, Point-Free, Set-Free Concrete Linear Algebra, International Conference on Interactive Theorem Proving, pp.103-118
DOI : 10.1017/S0956796802004501

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

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A Machine-Checked Proof of the Odd Order Theorem, ITP 2013, 4th Conference on Interactive Theorem Proving, pp.163-179, 2013.
DOI : 10.1007/978-3-642-39634-2_14

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

L. M. Goodman, Tezos: A self-amending crypto ledger position paper, 2014.

M. Gordon, R. Milner, and C. Wadsworth, Edinburgh LCF: a mechanized logic of computation, Lecture Notes in Computer Science, vol.78, pp.1-6, 1979.
DOI : 10.1007/3-540-09724-4

X. Gourdon, The 10 13 first zeros of the Riemann Zeta function, and zeros computation at very large height, 2004.

T. Gowers and M. Nielsen, Massively collaborative mathematics, Nature, vol.3, issue.7266, pp.461879-881, 2009.
DOI : 10.1038/461879a

B. Grégoire and X. Leroy, A compiled implementation of strong reduction, Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming, ICFP '02, pp.235-246, 2002.

B. Grégoire, L. Théry, and B. Werner, A Computational Approach to Pocklington Certificates in Type Theory, pp.97-113
DOI : 10.1007/978-1-4613-0041-0

T. Hales, M. Adams, G. Bauer, T. D. Dang, J. Harrison et al., A FORMAL PROOF OF THE KEPLER CONJECTURE, Forum of Mathematics, Pi, vol.41, 2017.
DOI : 10.1007/978-3-642-03359-9_4

C. Thomas and . Hales, The Kepler conjecture. arXiv preprint math, 1998.

C. Thomas and . Hales, Mathematics in the age of the Turing machine, 2014.

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.1142/4132

J. Harrison, Formal Proofs of Hypergeometric Sums, Journal of Automated Reasoning, vol.3, issue.3, pp.223-243, 2015.
DOI : 10.1016/0377-0427(90)90042-X

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

J. Hass and R. Schlafly, Double Bubbles Minimize, The Annals of Mathematics, vol.151, issue.2, pp.459-515, 2000.
DOI : 10.2307/121042

URL : http://arxiv.org/pdf/math/0003157

M. Hedberg, A coherence theorem for Martin-L??f's type theory, Journal of Functional Programming, vol.8, issue.4, pp.413-436, 1998.
DOI : 10.1017/S0956796898003153

A. Dennis, A. M. Hejhal, and . Odlyzko, Alan Turing and the Riemann zeta function. Alan Turing: His Work and Impact, pp.265-279, 2012.

H. A. Helfgott, Rigorous numerical integration URL:https://mathoverflow, MathOverflow, 123677.

H. A. Helfgott, Major arcs for Goldbach's problem, 1305.

A. Harold and . Helfgott, The ternary Goldbach conjecture is true (2013). arXiv preprint, 2014.

J. H. Marijn, O. Heule, V. W. Kullmann, and . Marek, Solving and verifying the boolean pythagorean triples problem via cube-and-conquer

F. Hivert, Coq-combi. https://github.com/hivert

J. Hölzl, F. Immler, and B. Huffman, Type Classes and Filters for Mathematical Analysis in Isabelle, pp.279-294, 2013.

M. Hutchings, F. Morgan, M. Ritoré, and A. R. , Proof of the Double Bubble Conjecture, The Annals of Mathematics, vol.155, issue.2, pp.459-489, 2002.
DOI : 10.2307/3062123

F. Immler, Formally Verified Computation of Enclosures of Solutions of Ordinary Differential Equations, NASA Formal Methods (NFM), pp.113-127, 2014.
DOI : 10.1007/978-3-319-06200-6_9

M. Mioara and . Joldes, Rigorous Polynomial Approximations and Applications. Theses, Ecole normale supérieure de lyon -ENS LYON, 2011.

. M. Mikhail, V. A. Kapranov, and . Voevodsky, ?-groupoids and homotopy types, pp.29-46, 1991.

E. Donald and . Knuth, Dancing links. arXiv preprint cs, 2000.

L. Lamport, LATEX: a document preparation system: user's guide and reference manual, 1994.

L. François and . Gall, Powers of tensors and fast matrix multiplication, Proceedings of the 39th international symposium on symbolic and algebraic computation, pp.296-303, 2014.

C. Lelay, Repenser la bibliothèque réelle de Coq: vers une formalisation de l'analyse classique mieux adaptée, 2015.

X. Leroy, D. Doligez, A. Frisch, J. Garrigue, D. Rémy et al., The OCaml system (release 3.12): Documentation and user's manual, Institut National de Recherche en Informatique et en Automatique, 2011.

V. Magron, NLCertify: A Tool for Formal Nonlinear Optimization, International Congress on Mathematical Software, pp.315-320, 2014.
DOI : 10.1007/978-3-662-44199-2_49

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

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

A. Mahboubi, G. Melquiond, and T. Sibut-pinote, Formally Verified Approximations of Definite Integrals, Proceedings of the 7th Conference on Interactive Theorem Proving, pp.274-289, 2016.
DOI : 10.1017/S096249291000005X

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

A. Mahboubi, G. Melquiond, and T. Sibut-pinote, Formally Verified Approximations of Definite Integrals, Accepted in Journal of Automated Reasoning, S.I : ITP 2016, 2017.
DOI : 10.1017/S096249291000005X

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

A. Mahboubi and E. Tassi, Canonical Structures for the Working Coq User, ITP 2013, 4th Conference on Interactive Theorem Proving, pp.19-34, 2013.
DOI : 10.1007/978-3-642-39634-2_5

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

E. Makarov and B. Spitters, The Picard Algorithm for Ordinary Differential Equations in Coq, Interactive Theorem Proving (ITP), pp.463-468, 2013.
DOI : 10.1007/978-3-642-39634-2_34

K. Makino and M. Berz, Taylor models and other validated functional inclusion methods, Int. J. Pure Appl. Math, 2003.

E. Martin-dorel and G. Melquiond, Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq, Journal of Automated Reasoning, vol.17, issue.3, pp.1-31, 2015.
DOI : 10.1145/114697.116813

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

M. Mayero, Formalisation et automatisation de preuves en analyses réelle et numérique, 2001.

M. Mayero, Using theorem proving for numerical analysis. Lecture notes in computer science, pp.246-262, 2002.
DOI : 10.1007/3-540-45685-6_17

R. Milner, The definition of standard ML: revised, 1997.

S. Nakamoto, Bitcoin: A peer-to-peer electronic cash system

S. Nedialko and . Nedialkov, Interval tools for ODEs and DAEs, Scientific Computing, 2006.

O. Russell, B. Connor, and . Spitters, A computer verified, monadic, functional implementation of the integral, Theoretical Computer Science, vol.411, issue.37, pp.3386-3402, 2010.

V. Pan, How to multiply matrices faster, 1984.
DOI : 10.1007/3-540-13866-8

C. Lawrence and . Paulson, Isabelle: A generic theorem prover, 1994.

J. D. Phillips and D. Stanovsk, Stanovsk`y. Using automated theorem provers in nonassociative algebra, 2008.

T. Piezas, Ramanujan's constant (e ? ? 163) and its cousins

D. H. Polymath, The " bounded gaps between primes " polymath projecta retrospective. arXiv preprint, 2014.

L. Pottier, Connecting Gröbner bases programs with Coq to do proofs in algebra, geometry and arithmetics. CoRR, abs/1007, 2010.

T. Rivoal, Propriétés diophantiennes de la fonction zêta de Riemann aux entiers impairs, 2001.

W. Romberg, Vereinfachte numerische integration Det Kongelige Norske Videnskabers Selskab Forhandlinger, pp.30-36, 1955.

S. M. Rump, Verification methods, Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation, ISSAC '10, pp.287-449, 2010.
DOI : 10.1145/1837934.1837937

R. El-siba¨?esiba¨?e and J. Filliâtre, Combine: an ocaml library for combinatorics, 2016.

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

B. Salvy and P. Zimmermann, GFUN: a Maple package for the manipulation of generating and holonomic functions in one variable, ACM Transactions on Mathematical Software, vol.20, issue.2, pp.163-177, 1994.
DOI : 10.1145/178365.178368

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

A. Schönhage, Partial and Total Matrix Multiplication, SIAM Journal on Computing, vol.10, issue.3, pp.434-455, 1981.
DOI : 10.1137/0210032

C. Simpson, Homotopy types of strict 3-groupoids. arXiv:math/9810059, 1998.

J. Spolsky and J. Atwood, Math Overflow. https://mathoverflow, 2008.

V. Strassen, Gaussian elimination is not optimal. Numerische mathematik, pp.354-356, 1969.
DOI : 10.1007/bf02165411

V. Strassen, Relative bilinear complexity and matrix multiplication, Journal für die reine und angewandte Mathematik, pp.406-443, 1987.

N. Swamy, C. Hrit¸cuhrit¸cu, A. Keller, A. Rastogi, S. Delignat-lavaud et al., Dependent types and multi-monadic effects in F*, 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp.256-270, 2016.
DOI : 10.1145/2914770.2837655

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

W. Tucker, The Lorenz attractor exists Comptes Rendus de l'Académie des Sciences-Series I-Mathematics, pp.1197-1202, 1999.

W. Tucker, Validated Numerics: A Short Introduction to Rigorous Computations, 2011.
DOI : 10.4171/009-1/54

S. Henry, What is the mistake in the proof of the homotopy hypothesis by Kapranov and Voevodsky? MathOverflow. Url: https://mathoverflow, pp.234492-2017, 22131.

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

A. Vladimir and . Voevodsky, Univalent foundations. http://www.math.ias

A. North and W. , An introduction to mathematics, 2017.

F. Wiedijk, The Seventeen Provers of the World, Lecture Notes in Computer Science / Lecture Notes in Artificial Intelligence, vol.3600, 2006.
DOI : 10.1007/11542384

V. V. Williams, Multiplying matrices faster than coppersmith-winograd, Proceedings of the 44th symposium on Theory of Computing, STOC '12, pp.887-898, 2012.
DOI : 10.1145/2213977.2214056

URL : http://www.eecs.berkeley.edu/~virgi/matrixmult-f.pdf

S. Winograd, On multiplication of 2× 2 matrices. Linear algebra and its applications, pp.381-388, 1971.

W. Woan, L. Shapiro, and D. G. Rogers, The catalan numbers, the lebesgue integral, and 4n-2, American Mathematical Monthly, pp.926-931, 1997.
DOI : 10.2307/2974473

G. Wood, Ethereum: A secure decentralised generalised transaction ledger, 2013.

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

URL : https://doi.org/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

B. Ziliani, D. Dreyer, N. R. Krishnaswami, A. Nanevski, and V. Vafeiadis, Mtac, ACM SIGPLAN Notices, vol.48, issue.9, pp.87-100, 2013.
DOI : 10.1145/2544174.2500579

A. Table, Best Complexities of Pan's tensor (presented in Section 4.4.3) with parameters m and p varying from 2 to 15