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.
- 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.
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).
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.
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.
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
./mill -i nlp.repl
for the natural language processing part.
To experiment with natural language processing, a basic server can be started by running
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
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/binfolder. The first time you do this, you may need to run
mkdir notes/binin the shell first (should not be needed anymore).
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.