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 notes folder contains Jupyter notebooks illustrating some of the code.
- Some documentation is in the project wiki.
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
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 [https://git-scm.com/book/en/v2/Git-Tools-Submodules#_cloning_submodules](update submodule).
To pop up a console with most of the code in scope, install mill and run:
mill -i mantle.repl
for the HoTT implementation etc, or
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