Méthodes matricielles -Introductionàtroduction`troductionà la complexité algébrique, Mathématiques et Applications, 2003. ,
Ahmed's integral: the maiden solution, Mathematical Spectrum, vol.48, issue.1, pp.11-12, 2015. ,
Every planar map is four colorable . part i: Discharging, Illinois Journal of Mathematics, vol.21, issue.3, pp.429-490, 1977. ,
Irrationalité de ?(2) et ?(3) Astérisque, 61, 1979. ,
A formally verified proof of the prime number theorem, ACM Transactions on Computational Logic, vol.9, issue.1, 2007. ,
DOI : 10.1145/1297658.1297660
Autarkic computations in formal proofs, Journal of Automated Reasoning, vol.28, issue.3, pp.321-336, 2002. ,
DOI : 10.1023/A:1015761529444
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
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
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
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
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
Fast Reflexive Arithmetic Tactics the Linear Case and Beyond, TYPES'06, pp.48-62, 2007. ,
DOI : 10.1007/978-3-540-74464-1_4
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
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. ,
Formalizing a proof that e is transcendental, Journal of Formalized Reasoning, vol.4, issue.1, pp.71-84, 2011. ,
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
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
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
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
Eléments de mathématique : Livre III. Topologie générale, 1968. ,
Algebraic complexity theory, 2013. ,
DOI : 10.1007/978-3-662-03338-8
Filtres et ultrafiltres Comptes Rendus Hebdomadaires des Séances de l'Académie des Sciences, pp.777-779, 1937. ,
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
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
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
Formalized algebraic numbers: construction and first-order theory ,
URL : https://hal.archives-ouvertes.fr/pastel-00780446
Refinements for Free! In Certified Programs and Proofs, pp.147-162, 2013. ,
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
Démonstration de l'irrationalité de ? (3)(d'apres apéry) ,
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
Adaptive, self-validating numerical quadrature, SIAM Journal on Scientific and Statistical Computing, vol.8, issue.5, pp.831-847, 1987. ,
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
Chapter 4 -error analysis, Methods of Numerical Integration, pp.271-343, 1984. ,
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
Fast matrix multiplication and symbolic computation. CoRR, abs, 1612. ,
URL : https://hal.archives-ouvertes.fr/hal-01417524
GNU Octave version 3.8.1 manual: a high-level interactive language for numerical computations, 2014. ,
Extending smtcoq, a certified checker for smt, 2016. ,
DOI : 10.4204/eptcs.210.5
URL : https://hal.archives-ouvertes.fr/hal-01388984
Observations on a certain theorem of Fermat and on others concerning prime numbers. ArXiv Mathematics e-prints, 2005. ,
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
Irrationalité de valeurs de zêta (d'après, Séminaire Bourbaki Exposés 909?923, pp.27-62, 2002. ,
Intégration numérique avec erreur bornée en précision arbitraire, 2006. ,
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
The bitcoin backbone protocol: Analysis and applications, EUROCRYPT, pp.281-310, 2015. ,
Computers and intractability, wh freeman, vol.29, 2002. ,
The Four Colour Theorem: Engineering of a Formal Proof, Computer Mathematics, pp.333-333, 2008. ,
DOI : 10.1007/978-3-540-87827-8_28
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
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
Tezos: A self-amending crypto ledger position paper, 2014. ,
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
The 10 13 first zeros of the Riemann Zeta function, and zeros computation at very large height, 2004. ,
Massively collaborative mathematics, Nature, vol.3, issue.7266, pp.461879-881, 2009. ,
DOI : 10.1038/461879a
A compiled implementation of strong reduction, Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming, ICFP '02, pp.235-246, 2002. ,
A Computational Approach to Pocklington Certificates in Type Theory, pp.97-113 ,
DOI : 10.1007/978-1-4613-0041-0
A FORMAL PROOF OF THE KEPLER CONJECTURE, Forum of Mathematics, Pi, vol.41, 2017. ,
DOI : 10.1007/978-3-642-03359-9_4
The Kepler conjecture. arXiv preprint math, 1998. ,
Mathematics in the age of the Turing machine, 2014. ,
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
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
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
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
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
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
Alan Turing and the Riemann zeta function. Alan Turing: His Work and Impact, pp.265-279, 2012. ,
Rigorous numerical integration URL:https://mathoverflow, MathOverflow, 123677. ,
Major arcs for Goldbach's problem, 1305. ,
The ternary Goldbach conjecture is true (2013). arXiv preprint, 2014. ,
Solving and verifying the boolean pythagorean triples problem via cube-and-conquer ,
Coq-combi. https://github.com/hivert ,
Type Classes and Filters for Mathematical Analysis in Isabelle, pp.279-294, 2013. ,
Proof of the Double Bubble Conjecture, The Annals of Mathematics, vol.155, issue.2, pp.459-489, 2002. ,
DOI : 10.2307/3062123
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
Rigorous Polynomial Approximations and Applications. Theses, Ecole normale supérieure de lyon -ENS LYON, 2011. ,
?-groupoids and homotopy types, pp.29-46, 1991. ,
Dancing links. arXiv preprint cs, 2000. ,
LATEX: a document preparation system: user's guide and reference manual, 1994. ,
Powers of tensors and fast matrix multiplication, Proceedings of the 39th international symposium on symbolic and algebraic computation, pp.296-303, 2014. ,
Repenser la bibliothèque réelle de Coq: vers une formalisation de l'analyse classique mieux adaptée, 2015. ,
The OCaml system (release 3.12): Documentation and user's manual, Institut National de Recherche en Informatique et en Automatique, 2011. ,
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
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
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
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
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
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
Taylor models and other validated functional inclusion methods, Int. J. Pure Appl. Math, 2003. ,
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
Formalisation et automatisation de preuves en analyses réelle et numérique, 2001. ,
Using theorem proving for numerical analysis. Lecture notes in computer science, pp.246-262, 2002. ,
DOI : 10.1007/3-540-45685-6_17
The definition of standard ML: revised, 1997. ,
Bitcoin: A peer-to-peer electronic cash system ,
Interval tools for ODEs and DAEs, Scientific Computing, 2006. ,
A computer verified, monadic, functional implementation of the integral, Theoretical Computer Science, vol.411, issue.37, pp.3386-3402, 2010. ,
How to multiply matrices faster, 1984. ,
DOI : 10.1007/3-540-13866-8
Isabelle: A generic theorem prover, 1994. ,
Stanovsk`y. Using automated theorem provers in nonassociative algebra, 2008. ,
Ramanujan's constant (e ? ? 163) and its cousins ,
The " bounded gaps between primes " polymath projecta retrospective. arXiv preprint, 2014. ,
Connecting Gröbner bases programs with Coq to do proofs in algebra, geometry and arithmetics. CoRR, abs/1007, 2010. ,
Propriétés diophantiennes de la fonction zêta de Riemann aux entiers impairs, 2001. ,
Vereinfachte numerische integration Det Kongelige Norske Videnskabers Selskab Forhandlinger, pp.30-36, 1955. ,
Verification methods, Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation, ISSAC '10, pp.287-449, 2010. ,
DOI : 10.1145/1837934.1837937
Combine: an ocaml library for combinatorics, 2016. ,
An Algolib-aided version of Apéry's proof of the irrationality of ?(3), 2003. ,
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
Partial and Total Matrix Multiplication, SIAM Journal on Computing, vol.10, issue.3, pp.434-455, 1981. ,
DOI : 10.1137/0210032
Homotopy types of strict 3-groupoids. arXiv:math/9810059, 1998. ,
Math Overflow. https://mathoverflow, 2008. ,
Gaussian elimination is not optimal. Numerische mathematik, pp.354-356, 1969. ,
DOI : 10.1007/bf02165411
Relative bilinear complexity and matrix multiplication, Journal für die reine und angewandte Mathematik, pp.406-443, 1987. ,
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
The Lorenz attractor exists Comptes Rendus de l'Académie des Sciences-Series I-Mathematics, pp.1197-1202, 1999. ,
Validated Numerics: A Short Introduction to Rigorous Computations, 2011. ,
DOI : 10.4171/009-1/54
What is the mistake in the proof of the homotopy hypothesis by Kapranov and Voevodsky? MathOverflow. Url: https://mathoverflow, pp.234492-2017, 22131. ,
Ap??ry???s Proof of the irrationality of ??(3), The Mathematical Intelligencer, vol.1, issue.4, pp.195-203, 1979. ,
DOI : 10.1007/BF03028234
Univalent foundations. http://www.math.ias ,
An introduction to mathematics, 2017. ,
The Seventeen Provers of the World, Lecture Notes in Computer Science / Lecture Notes in Artificial Intelligence, vol.3600, 2006. ,
DOI : 10.1007/11542384
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
On multiplication of 2× 2 matrices. Linear algebra and its applications, pp.381-388, 1971. ,
The catalan numbers, the lebesgue integral, and 4n-2, American Mathematical Monthly, pp.926-931, 1997. ,
DOI : 10.2307/2974473
Ethereum: A secure decentralised generalised transaction ledger, 2013. ,
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
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
Mtac, ACM SIGPLAN Notices, vol.48, issue.9, pp.87-100, 2013. ,
DOI : 10.1145/2544174.2500579
Best Complexities of Pan's tensor (presented in Section 4.4.3) with parameters m and p varying from 2 to 15 ,