ProvingGround

ProvingGround copied to clipboard

Deep learning: why, how

7

## Optimization vs deep learning * We can optimize generation when this is in terms of known elements and equations. * We can extend this by smoothing goals, for example....

siddhartha-gadgil

Representation learning or Vector Embedding

10

There are many ways in which, given a (weighted) collection of linear terms, we can generate weighted graphs. Namely, we traverse based on: - combinations of terms: function application, lambdas...

siddhartha-gadgil

Increasing range of terms parsable into MathExpr

9

The following is a list of issues which need to be fixed/improved on in the parser for `MathExpr` - [ ] Issues relating to the verb of the clause being...

sundararajan-s

Simplify induction to Recursion

9

* In many cases, especially from lean, a function is defined as inductive depending on a family, e.g. `cases_on`. * Subsequently this is applied to a constant family. * In...

siddhartha-gadgil

Separate equations with initial values

2

* Storing and recalling them is misleading. * On the other hand, when initializing with a term state one must generate and include the corresponding equations. * __Warning:__ we do...

siddhartha-gadgil

Abstraction, generalization, common results

2

* This includes #221 - using results from experiments. * To rewrite one or more statements - identify complex terms that are parts of statements and proofs. - generate functions...

siddhartha-gadgil

Type level definition data

3

* The `avoidVar` method should cover products etc. * Since `defnData` is used in `fromData`, presently with a lot of casting, it should be upgraded to a `TermList`. * We...

siddhartha-gadgil