“DeepMath: Deep Sequence Models for Premise Selection”, 2016-06-14 (; similar):
We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics.
We propose a 2-stage approach for this task that yields good results for the premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing state-of-the-art models.
To our knowledge, this is the first time deep learning has been applied to theorem proving on a large scale.