First Neural Conjecturing Datasets and Experiments
This work addresses the challenge of automated theorem proving for mathematicians and AI researchers, but it is incremental as it builds on existing datasets and methods.
The authors tackled the problem of generating mathematical conjectures using neural methods by creating datasets from the Mizar Mathematical Library and conducting initial experiments with Transformer architectures like GPT-2, resulting in the first datasets and experiments in this area without specific numerical results reported.
We describe several datasets and first experiments with creating conjectures by neural methods. The datasets are based on the Mizar Mathematical Library processed in several forms and the problems extracted from it by the MPTP system and proved by the E prover using the ENIGMA guidance. The conjecturing experiments use the Transformer architecture and in particular its GPT-2 implementation.