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 ...