Theory Exploration
By now MMT is strong enough to generate values of arbitrary types and compute with them.
This can be used for a generic theory exploration algorithm: Generate a formula, generate some values, test the formula. If the formula is true for all values, it may be a theorem and is marked as such.
Later a human or a theorem can inspect the generated theorems and add the proofs.
For example, consider addition on the natural numbers with +, 0, and =. MMT can generate formulas by
- using some (e.g., up to 3) free variables x,y,z
- systematically generate well-typed terms from them such as x, y, z, x+y, y+x, x+z, z+x, x+z, y+z, z+y, x+0, 0+x, and so on
- systematically generate values of N such as 0, 1, 3, 10, 13
- plug in all combinations of the values for x, y, z into the generated terms
- whenever two terms t(x,y,z) and t'(x,y,z) that agree on all values and conjecture the theorem forall xy.t(x,y,z)=t'(x,y,z)
Many important theorems can be guessed in this way, and for not-well-understood-yet theories, it's plausible that will include some new theorems.
There is already prior work on conjecture generation, historically by Simon Colton (look it up) and more recently by Josef Urban, Cezary Kaliszyck. The latter is quite compatible with this idea but is on different corpora.