In my work I have developed a learning-based method that enhances the efficiency and accuracy of automatic theorem proving. Inspired by the research of Urban et al. (2020).

Central to my methodology is the use of a long short-term memory (LSTM) architecture, along with general attention and beam search mechanisms. By leveraging the internal state vector of the LSTM, which updates with each chosen fact, the model achieves decision-making capabilities that mimic the state of a proof.

Additionally, I explore the integration of formula embedding techniques with various machine learning (ML) models, specifically investigating the combination with GloVe. This integration enhances the theorem proving capabilities of the LSTM architecture.

Compared to the original approach, my method demonstrates a 5% increase in proven theorems.

Alongside my research, I provide a comprehensive overview of automatic theorem proving and its connection to machine learning.

Orientador: Pedro A. Santos