# ProvingGround: Automated Theorem proving by learning

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.

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

## Foundations

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.

## Learning and reflection

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.

## Lean theorem prover interaction

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.

## 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. 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). 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

• HoTT expressions
• val definitions

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


## 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).