First Neural Conjecturing Datasets and Experiments
  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.
