Automated Reasoning in Large Theories and Premise Selection with Machine Learning

In the talk I will briefly overview current state-of-the-art in the
fields of Formal Mathematics and Automated Theorem Proving and how
Machine Learning techniques can be fruitfully applied in these
domains. One of crucial problems when automatically proving theorems
in formal mathematical library is premise selection task, and machine
learning is very useful there. I will show the results of my recent
experiments of performing Premise Selection with use of Gradient
Boosted Trees, on Mizar Mathematical Library.

Preprint with the results: https://arxiv.org/abs/1802.03375 <--
submitted to a major conference in AI
Implementation of the system for experiments:
https://github.com/BartoszPiotrowski/ATPboost