siddhartha-gadgil / provingground

Proving Ground: Tools for Automated Mathematics

Website GitHub

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.

Build Status codecov.io Ohloh

Documentation:

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

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.

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

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