A Formal Proof of the Expressiveness of Deep Learning

Alexander Bentkamp*, Jasmin Christian Blanchette, Dietrich Klakow

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review


Deep learning has had a profound impact on computer science in recent years, with applications to image recognition, language processing, bioinformatics, and more. Recently, Cohen et al. provided theoretical evidence for the superiority of deep learning over shallow learning. We formalized their mathematical proof using Isabelle/HOL. The Isabelle development simplifies and generalizes the original proof, while working around the limitations of the HOL type system. To support the formalization, we developed reusable libraries of formalized mathematics, including results about the matrix rank, the Borel measure, and multivariate polynomials as well as a library for tensor analysis.

Original languageEnglish
Pages (from-to)347-368
Number of pages22
JournalJournal of Automated Reasoning
Issue number2
Publication statusPublished - Aug 2019


  • Isabelle
  • HOL
  • Deep learning
  • Machine learning
  • Convolutional arithmetic circuits
  • Formalization
  • Tensors


Dive into the research topics of 'A Formal Proof of the Expressiveness of Deep Learning'. Together they form a unique fingerprint.

Cite this