ProvingGround

Proving Ground: Tools for Automated Mathematics

A system under development for (semi-)automated theorem proving, with foundations homotopy type theory, using machine learning, both by reinforcement learing using backward-propagation and using natural language processing to assimilate part of the mathematics literature.

Documentation

• The main documentation is on the website , including scaladocs. The same site also hosts working notes.
• The notes folder contains Jupyter notebooks illustrating some of the code.
• Some documentation is in the project wiki.

Try it with zero installation

You can try the project with zero installation on scastie, for example the HoTT worksheet. If you want to try your own worksheet add the library provvingground-core-jvm (which can be found with scastie's search). More worksheets and info will be posted soon.

Contributors

This project has greatly benefited by contributions from

• Dymtro Mitin
• Tomoaki Hashizaki
• Olivier Roland
• Sayantan Khan

The principal developer is Siddhartha Gadgil (Department of Mathematics, Indian Institute of Science, Bangalore).

Running

Servers

Two rudimentary servers are available as binaries, which you can download and run. You need Java 8 installed. In Unix systems you may need to run chmod +x ... to make the files executable.

• ProvingGround HoTT Server
• ProvingGround NLP Server

Start one of these servers and visit localhost:8080 on a browser to run. You can also specify the port by starting with a -p option (and interface using -i). Note that the second server also includes most of the first server.

These will be frequently updated with new features.

From Source

At present the best way to interact with most of the code is to use a console in either mill or sbt (the primary build tool is now mill).
Note that trepplein is a git submodule and is a dependency of part of the code, so you will have to clone submodules.
The simpliest way to do this is to clone the project with submodules :

git clone --recurse-submodules --single-branch https://github.com/siddhartha-gadgil/ProvingGround.git

or if you have already clone the project without submodules, you can fetch them afterwards :

git submodule update --init

To pop up a console with the core code in scope, run (you need Java 8 installed, but mill need not be installed as it has a bootstrap script):

./mill -i core.jvm.repl

For running with some IO code (e.g. parsing lean exports), instead run

./mill -i mantle.repl

and

./mill -i nlp.repl

for the natural language processing part.

To experiment with natural language processing, a basic server can be started by running

./mill nlp.run

and going to localhost:8080 on the browser. To experiment with the code, you can use the --watch flag so the system restarts after shutting down from the browser.

Similarly, one can experiment with a small part of the HoTT implementation by running

./mill mantle.run

Using a Notebook interface

A useful way to experiment is to use a notebook instead of a repl session to ensure persistence. To do this:

• Install Jupyter and the almond kernel
• Generate a binary in the notes/bin folder. The first time you do this, you may need to run mkdir notes/bin in the shell first (should not be needed anymore).

./mill core.jvm.bin

This generates the binary and gives the command to use in jupyter-lab or the classic jupyter notebook. Note that you must launch jupyter-lab in the notes folder.

To replicate the behaviour of a notebook (generated this way) with the same source, note that the first code line shows the git has, for example from import $cp.bin.provingground-core-jvm-686ded3e77.fat.jar we see that the git hash is 686ded3e77. To use the jar for this version, run the following

git checkout 686ded3e77
./mill core.jvm.bin

You can then run the notebook.