First Neural Conjecturing Datasets and Experiments

TL;DR

This paper introduces datasets derived from the Mizar Mathematical Library and presents initial experiments using Transformer-based neural models, specifically GPT-2, to generate mathematical conjectures.

Contribution

It provides the first datasets for neural conjecturing in mathematics and demonstrates initial experiments with Transformer models for conjecture generation.

Findings

Datasets based on Mizar library and proof problems created.

Initial experiments with GPT-2 show potential for neural conjecturing.

Establishes a foundation for future neural conjecture research.

Abstract

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.