While the discovery process involves actual manipulation of terms, we refine using a reflection process, involving working with a large list of already discovered terms and their relations. The goal of this process is to efficiently encode mathematical knowledge, and especially to identify important theorems and concepts as well their relations.
Assume that we are given a distribution on types and we wish to find the best generating model.
Best is based on:
The model itself is:
We build this graph automatically, with a recursive definition. The entities are:
Variables
Placeholders/constants: for the generated probabilities of types.
Calculated expressions:
Optimization cost: combination of
Recursive definitions:
Multi-stage discovery: