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.
- Most of Homotopy type theory.
- Reinforcement learning abstractions.
- Dynamics for learning in a domain-specific case - the andrews-curtis conjecture.
- Most of the dynamics for learning with homotopy type theory.
- An akka-actor based system for continuous learning with tuning and communication.
- Skeletons of:
- an akka-http server
- a play-framework server
- using stanford-corenlp tools.
There is not much besides the source.
- The website has the most current documentation.
- The notes folder contains Jupyter notebooks illustrating some of the code.
- Some documentation is in the project wiki.
At present the only way to run the code is to load a console. For example, in the home of the project, run
sbt mantle/test:console
to pop up a nice console (Li Haoyi's ammonite repl), with many imports already in scope.