Experiments towards neural network theorem proving
Switch branches/tags
Nothing to show
Clone or download
Niklas Een
Niklas Een Sync
Latest commit 722917a Nov 13, 2017



The Deepmath project seeks to improve automated theorem proving using deep learning and other machine learning techniques. Deepmath is a collaboration between Google Research and several universities.


The source code in this repository is not an official Google product, but is a research collaboration with external research teams.

For now the repository contains only a C++ implementation of the HOL Light kernel, which we have released early in order to faciliate existing collaborations. More to come soon, including neural network models.


  • hol: A C++ implementation of the HOL Light kernel.
  • zz: A reimplementation of the HOL Light kernel (with visualizer and other stuff).


Deepmath depends on TensorFlow, which is included as a submodule. To use, first install all TensorFlow dependencies and run configure to initialize the build system, as described here:

# Install TensorFlow dependencies if necessary
cd deepmath/tensorflow
./configure  # and answer all questions

You can then build hol via

cd deepmath/hol
bazel build ...