B. W. Bader and T. G. Kolda, Algorithm 862: MATLAB tensor classes for fast algorithm prototyping, ACM Trans. Math. Softw, vol.32, issue.4, pp.635-653, 2006.

A. Bentkamp, Expressiveness of deep learning. Archive of Formal Proofs, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01599172

A. Bentkamp, An Isabelle formalization of the expressiveness of deep learning, 2016.

A. Bentkamp, J. C. Blanchette, and D. Klakow, A formal proof of the expressiveness of deep learning, Interactive Theorem Proving (ITP 2017), vol.10499, pp.46-64, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01599172

S. Bernard, Y. Bertot, L. Rideau, and P. Strub, Formal proofs of transcendence for e and ? as an application of multivariate and symmetric polynomials, Certified Programs and Proofs (CPP 2016), pp.76-87, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01240025

Y. Bertot, G. Gonthier, S. O. Biha, and I. Pasca, Canonical big operators, Theorem Proving in Higher Order Logics, vol.5170, pp.86-101, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00331193

S. Bhat, Syntactic foundations for machine learning, 2013.

J. C. Blanchette, S. Böhme, M. Fleury, S. J. Smolka, and A. Steckermeier, Semi-intelligible Isar proofs from machine-generated proofs, J. Autom. Reasoning, vol.56, issue.2, pp.155-200, 2016.
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, J. Autom. Reasoning, vol.57, issue.3, pp.219-244, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01386986

J. Boender, F. Kammüller, and R. Nagarajan, Formalization of quantum protocols using Coq, Workshop on Quantum Physics and Logic (QPL 2015), vol.195, pp.71-83, 2015.

S. Böhme and T. Weber, Fast LCF-style proof reconstruction for Z3, Interactive Theorem Proving (ITP 2010), vol.6172, pp.179-194, 2010.

P. Bürgisser, F. Cucker, and M. Lotz, The probability that a slightly perturbed numerical analysis problem is difficult, Math. Comput, vol.77, issue.263, pp.1559-1583, 2008.

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

A. Church, A formulation of the simple theory of types, J. Symb. Log, vol.5, issue.2, pp.56-68, 1940.

N. Cohen, O. Sharir, and A. Shashua, Deep SimNets, Computer Vision and Pattern Recognition (CVPR 2016), pp.4782-4791, 2016.

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, vol.49, pp.698-728, 2016.

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

N. Cohen and A. Shashua, Inductive bias of deep convolutional networks through pooling geometry, 2016.

N. Cohen, R. Tamari, and A. Shashua, Boosting dilated convolutional networks with mixed tensor decompositions, 2017.

M. J. Gordon, R. Milner, and C. P. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation, vol.78, 1979.

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

M. Hardt, B. Recht, and Y. Singer, Train faster, generalize better: Stability of stochastic gradient descent, International Conference on Machine Learning (ICML 2016, vol.48, pp.1225-1234, 2016.

J. Harrison, A HOL theory of Euclidean space, Theorem Proving in Higher Order Logics, vol.3603, pp.114-129, 2005.

J. Hölzl and A. Heller, Three chapters of measure theory in Isabelle/HOL, Interactive Theorem Proving (ITP 2011), 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, 2007.

K. Kawaguchi, Deep learning without poor local minima, Advances in Neural Information Processing Systems (NIPS 2016), NIPS, vol.29, pp.586-594, 2016.

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 (ICFEM 2014), vol.8829, pp.316-331, 2014.

M. Lotz, On the volume of tubular neighborhoods of real algebraic varieties, Proc. Amer. Math. Soc, vol.143, issue.5, pp.1875-1889, 2015.

L. De-moura and N. Bjørner, Z3: An efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), vol.4963, pp.337-340, 2008.

C. Murphy, P. Gray, and G. Stewart, Verified perceptron convergence theorem, Machine Learning and Programming Languages, pp.43-50, 2017.

T. Nipkow and G. Klein, Concrete Semantics: With Isabelle/HOL, 2014.

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, vol.2283, 2002.

L. C. Paulson and J. C. Blanchette, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, International Workshop on the Implementation of Logics (IWIL-2010), vol.2, pp.1-11, 2012.

L. C. Paulson and K. W. Susanto, Source-level proof reconstruction for interactive theorem proving, Theorem Proving in Higher Order Logics, vol.4732, pp.232-245, 2007.

H. Poon and P. M. Domingos, Sum-product networks: A new deep architecture, Uncertainty in Artificial Intelligence (UAI 2011), pp.337-346, 2011.

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

D. Selsam, P. Liang, and D. L. Dill, Developing bug-free machine learning systems with formal mathematics, International Conference on Machine Learning, vol.70, pp.3047-3056, 2017.

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. Archive of Formal Proofs, 2015.

N. Tishby and N. Zaslavsky, Deep learning and the information bottleneck principle, Information Theory Workshop (ITW 2015), pp.1-5, 2015.

M. Wenzel, Isar-A generic interpretative approach to readable formal proof documents, Theorem Proving in Higher Order Logics (TPHOLs '99), vol.1690, pp.167-184, 1999.