B. W. Bader and T. G. Kolda, Algorithm 862, ACM Transactions on Mathematical Software, vol.32, issue.4, pp.635-653, 2006.
DOI : 10.1145/1186785.1186794

A. Bentkamp, Expressiveness of deep learning Archive of Formal Proofs, 2016.

A. Bentkamp, An Isabelle Formalization of the Expressiveness of Deep Learning, 2016.

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, pp.76-87, 2016.
DOI : 10.1023/A:1026518331905

Y. Bertot, G. Gonthier, S. O. Biha, and I. Pasca, Canonical Big Operators, Theorem Proving in Higher Order Logics, pp.86-101, 2008.
DOI : 10.1007/3-540-44659-1_29
URL : https://hal.archives-ouvertes.fr/inria-00331193

S. Bhat, Syntactic foundations for machine learning, Georgia Institute of Technology, 2013.

J. C. Blanchette, S. Böhme, M. Fleury, S. J. Smolka, and A. Steckermeier, Semi-intelligible Isar Proofs from Machine-Generated Proofs, Journal of Automated Reasoning, vol.27, issue.4, pp.155-200, 2016.
DOI : 10.1007/978-3-642-37036-6_12
URL : https://hal.archives-ouvertes.fr/hal-01211748

J. C. Blanchette, D. Greenaway, C. Kaliszyk, D. Kühlwein, and J. Urban, A Learning-Based Fact Selector for Isabelle/HOL, Journal of Automated Reasoning, vol.15, issue.1, pp.219-244, 2016.
DOI : 10.1142/S0218213006002588
URL : https://hal.archives-ouvertes.fr/hal-01386986

J. Boender, F. Kammüller, and R. Nagarajan, Formalization of Quantum Protocols using Coq, Electronic Proceedings in Theoretical Computer Science, vol.195, pp.71-83, 2015.
DOI : 10.4204/EPTCS.195.6
URL : http://arxiv.org/pdf/1511.01568

S. Böhme and T. Weber, Fast LCF-Style Proof Reconstruction for Z3, LNCS, vol.6172, pp.179-194, 2010.
DOI : 10.1007/978-3-642-14052-5_14

P. Bürgisser, F. Cucker, and M. Lotz, The probability that a slightly perturbed numerical analysis problem is difficult, Mathematics of Computation, vol.77, issue.263, pp.1559-1583, 2008.
DOI : 10.1090/S0025-5718-08-02060-7

R. Caron and T. Traynor, The zero set of a polynomial, 2005.

N. Cohen, O. Sharir, and A. Shashua, Deep SimNets, 2016 IEEE Conference on Computer Vision and Pattern Recognition (CVPR), pp.4782-4791, 2016.
DOI : 10.1109/CVPR.2016.517

N. Cohen, O. Sharir, and A. Shashua, On the expressive power of deep learning: A tensor analysis, Conference on Learning Theory (COLT 2016). JMLR Workshop and Conference Proceedings, pp.698-728, 2016.

N. Cohen and A. Shashua, Convolutional rectifier networks as generalized tensor decompositions, International Conference on Machine Learning (ICML 2016). JMLR Workshop and Conference Proceedings, pp.955-963, 2016.

N. Cohen and A. Shashua, Inductive bias of deep convolutional networks through pooling geometry, CoRR abs/1605, p.6743, 2016.

F. Haftmann, A. Lochbihler, and W. Schreiner, Towards abstract and executable multivariate polynomials in Isabelle, p.2014, 2014.

J. Harrison, A HOL Theory of Euclidean Space, Theorem Proving in Higher Order Logics, pp.114-129, 2005.
DOI : 10.1007/11541868_8

J. Hölzl and A. Heller, Three chapters of measure theory in Isabelle/HOL, LNCS, vol.6898, pp.135-151, 2011.

F. Immler and A. Maletzky, Gröbner bases theory Archive of Formal Proofs, 2016.

R. Kam, Case Studies in Proof Checking Master's thesis, 2007.

H. Kobayashi, L. Chen, and H. Murao, Groups, rings and modules, Archive of Formal Proofs, 2004.

L. Liu, V. Aravantinos, O. Hasan, and S. Tahar, On the Formal Analysis of HMM Using Theorem Proving, International Conference on Formal Engineering Methods, pp.316-331, 2014.
DOI : 10.1007/978-3-319-11737-9_21

M. Lotz, On the volume of tubular neighborhoods of real algebraic varieties, Proc. Amer, pp.1875-1889, 2015.
DOI : 10.1090/S0002-9939-2014-12397-5

L. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, TACAS 2008, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

T. Murphy, P. Gray, and G. Stewart, Certified convergent perceptron learning

L. C. Paulson and J. C. Blanchette, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers

L. C. Paulson and K. W. Susanto, Source-Level Proof Reconstruction for Interactive Theorem Proving, Theorem Proving in Higher Order Logics, pp.232-245, 2007.
DOI : 10.1007/978-3-540-74591-4_18
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.145.8845

H. Poon and P. M. Domingos, Sum-product networks: A new deep architecture, 2011 IEEE International Conference on Computer Vision Workshops (ICCV Workshops), pp.337-346, 2011.
DOI : 10.1109/ICCVW.2011.6130310
URL : http://arxiv.org/abs/1202.3732

T. V. Prathamesh, Tensor product of matrices Archive of Formal Proofs, 2016.

C. Sternagel and R. Thiemann, Executable multivariate polynomials Archive of Formal Proofs, 2010.

R. Thiemann and A. Yamada, Matrices, Jordan normal forms, and spectral radius theory Formal proof development, Archive of Formal Proofs, 2015.

M. Wenzel, Isar ??? A Generic Interpretative Approach to Readable Formal Proof Documents, Theorem Proving in Higher Order Logics (TPHOLs '99), pp.167-184, 1999.
DOI : 10.1007/3-540-48256-3_12