Matej Petković: Agda in machine-learnable format

Agda is a dependently typed functional programming language which can be also used as a proof assistant. In Agda a theorem is written as a type, and proved by an expression of the given type.

While composing the expression, we would like to take advantage of previously proved lemmas (auxiliary statements), but we may not remember their names, or worse, know which lemmas to use. We are thus planning to create a recommender system that would suggest lemmas, given the type and partially constructed expression.

In this seminar, we will see how some Agda libraries were converted into a machine-learnable format (s-expressions) from which a knowledge graphs was built. We shall also show some preliminary results of simple machine-learning approaches to the problem.