This is a system under development for automated theorem proving. More concretely, we take as the goal of automated theorem proving to equip computers with all the major capabilities used in discovering and proving mathematical results. Our goal is to complement the many software systems that are useful in doing mathematics, with a focus on missing capabilities.
The one success of this project so far has been its role in the Polymath 14 project.
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.
The foundations we use are Homotopy Type Theory combined with symbolic algebra. This is crucial to our approach as the result is proofs that are not much more complex than real world mathematics - as illustrated, for example, in the PolyMath lemma. Note that much of that note is the fully expanded proofs as reported by the system - the code describing the proofs is not long.
The conciseness of HoTT proofs is not only of practical value, but is conceptually important as we base learning on the complexity of mathematical proofs.
Much of the work done so far has been on the implementation of homotopy type theory in scala, with an attempt to capture in scala types significant amount of information about the HoTT types.
The system learns based on a generative model that not only matches the generated distribution with a desired one, but takes into account the complexity of the generative model. This allows one to judge whether newly discovered results are worthwhile.
Our goal is to interact with external systems. In particular, we have implemented interaction with the lean theorem prover, whereby the export format of lean is used (via trepplein) to generate code in our implementation of HoTT. This allows us to start with a library for learning as well as a target for natural lannguage processing.
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.
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). 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
Some experiments with the HoTT interface can be done in the scratchpad below.
The scratchpad below is a limited interpreter for our implementation of Homotopy Type Theory. At present it interprets
val definitionsAs an example (which you may wish to copy paste), the definition of the term corresponding to modus ponens is below.
// View 'A' and 'B' as propositions
val A = "A" :: Type
val B = "B" :: Type
val a = "a" :: A
val f = "f" :: (A ->: B) // the type A ->: B corresponds to A => B
// 'mp' proves A => ((A => B) => B)
val mp = a :-> (f :-> f(a))
This project has greatly benefited by contributions from
The principal developer is Siddhartha Gadgil (Department of Mathematics, Indian Institute of Science, Bangalore).