---
title: "First Neural Conjecturing Datasets and Experiments — Urban 2020"
description: "Urban and Jakubův build four datasets from the Mizar Mathematical Library (MML). 17 references, cited by 16 papers here."
authors: ["Josef Urban", "Jan Jakubův"]
year: 2020
venue: "arXiv:2005.14664"
source: "https://arxiv.org/abs/2005.14664"
doi: "10.48550/arxiv.2005.14664"
arxiv: "2005.14664"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "http://arxiv.org/licenses/nonexclusive-distrib/1.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/urban-2020-first-neural-conjecturing-datasets-experiments/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/urban-2020-first-neural-conjecturing-datasets-experiments/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2020](https://md.research.elamur.ai/free/en/papers/2020/page/7/) / First Neural Conjecturing Datasets and Experiments

# First Neural Conjecturing Datasets and Experiments

**Authors:** [Josef Urban](https://md.research.elamur.ai/free/en/authors/josef-urban/) and [Jan Jakubův](https://md.research.elamur.ai/free/en/authors/jan-jakubuv/) · **Year:** 2020 · **Venue:** [arXiv:2005.14664](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/) ([Lecture notes in computer science 2020](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/2020/)) · **Publisher:** [Springer Science+Business Media](https://md.research.elamur.ai/free/en/publishers/springer-science-business-media/) · **Licence:** [arXiv — non-exclusive licence to distribute](http://arxiv.org/licenses/nonexclusive-distrib/1.0/)

**Links:** [Publisher's page](https://arxiv.org/abs/2005.14664) · [PDF](https://arxiv.org/pdf/2005.14664) · [DOI 10.48550/arxiv.2005.14664](https://doi.org/10.48550/arxiv.2005.14664) · [arXiv 2005.14664](https://arxiv.org/abs/2005.14664) · [OpenAlex](https://openalex.org/W3029284261)

**Citations:** 24 citations (OpenAlex, 2026-10-14) · [16](https://md.research.elamur.ai/free/en/papers/urban-2020-first-neural-conjecturing-datasets-experiments/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
The paper addresses automated conjecture generation in large formal mathematics corpora. This covers proposing helpful intermediate lemmas and exploring a theory freely. Urban and Jakubův build four datasets from the Mizar Mathematical Library (MML). Two are textual: raw Mizar articles and an HTML-derived export enriched with types and theses. The other two come from MPTP-translated problems proved by the E prover with ENIGMA guidance: full tokenized TPTP proofs and compact prefix-notation lists of the premises each proof used. They train the smallest GPT-2 model on each dataset and test it in three ways: unconditioned sampling, conditioned completion of formulas and premise lists, and an ATP-based semantic evaluation. GPT-2 produces plausible Mizar-style theorems and proofs, and some of its suggested premise sets yield new E proofs. However, many outputs are unprovable or countersatisfiable, which exposes a gap between syntactic training loss and logical usefulness. The released datasets, models, samples and web autocompletion server give a first public basis for neural conjecturing and for future learning–reasoning feedback loops.

## Key points
- **Four datasets:**
  - MML version 1147 concatenated (78MB).
  - HTML-export text (156MB).
  - ENIGMA/E TPTP proofs for 28,271 theorems (658MB).
  - Prefix-notation premise selections (53MB).
- **Training setup:** GPT-2 with 117M parameters, trained on one GTX 1080 GPU. Training ran for weeks on datasets 1, 2 and 4. Training on dataset 3 was stopped early because of redundant punctuation tokens.
- **Conditioned completion:** The tests used 369 CARD theorems for premise completion and 462 partial CARD formulas for formula completion. Low sampling temperatures mostly reproduce existing Mizar theorems. Higher temperatures produce new well-typed lemmas, and still higher ones produce ill-typed or unparsable output.
- **ATP evaluation on 31,792 theorems (6639 unseen):**
  - 12 predictions per theorem gave 381,432 predictions, or 193,320 unique ones.
  - Of the problems without new conjectures, 86,899 of 108,564 were countersatisfiable.
  - 11,866 problems were proved within 6 s, covering 8105 theorems. Many of these proofs were trivial self-premise cases.
- **New formulas:** GPT-2 proposed 52,515 new syntactically correct formulas, 33,100 after deduplication. E with ENIGMA and standard premise selection proved about 9000–10000 of them. Some interesting conjectures were generalizations, for example from finite to arbitrary groups.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

## Cite

Cite as: Josef Urban and Jan Jakubův. 2020. First Neural Conjecturing Datasets and Experiments. arXiv:2005.14664.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{urban2020first,
  title = {{First Neural Conjecturing Datasets and Experiments}},
  author = {Josef Urban and Jan Jakubův},
  year = {2020},
  doi = {10.48550/arxiv.2005.14664},
  eprint = {2005.14664},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2005.14664}
}
```

- [← previous Dialogue Coherence Assessment Without Explicit Dialogue Act Labels](https://md.research.elamur.ai/free/en/papers/mesgar-2020-dialogue-coherence-assessment-without-explicit/)
- [next → The Hebrew of the Dead Sea Scrolls and the Tiberian Reading Tradition](https://md.research.elamur.ai/free/en/papers/hornkohl-2020-hebrew-dead-sea-scrolls-tiberian/)
- [↑ back to papers of 2020](https://md.research.elamur.ai/free/en/papers/2020/page/7/)

## References

17 references, 5 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Chad E. Brown and Thibault Gauthier. Self-learned formula synthesis in set theory. CoRR, abs/1912.01525, 2019. — [arXiv:1912.01525](https://arxiv.org/abs/1912.01525) [find](https://scholar.google.com/scholar?q=Chad+E%2E+Brown+and+Thibault+Gauthier%2E+Self%2Dlearned+formula+synthesis+in+set+theory%2E+CoRR%2C+abs%2F1912%2E01525%2C+2019%2E+%E2%80%94+%5BarXiv%3A1912%2E01525%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1912%2E01525%29)
2. Karel Chvalovský, Jan Jakubuv, Martin Suda, and Josef Urban. [ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E](https://md.research.elamur.ai/free/en/papers/chvalovsky-2019-enigma-ng-efficient-neural-gradient/). In CADE 27, pages 197–215, 2019.
3. Simon Colton. Automated Theory Formation in Pure Mathematics. Distinguished Dissertations. Springer London, 2012. [http://grid01.ciirc.cvut.cz/~mptp/nn_conj20/results/preddatagpt1.out.tar.gz](http://grid01.ciirc.cvut.cz/~mptp/nn_conj20/results/preddatagpt1.out.tar.gz) http://grid01.ciirc.cvut.cz/~mptp/nn_conj20/results/preddatagpt1.tar.gz http://grid01.ciirc.cvut.cz/~mptp/7.13… [↗](http://grid01.ciirc.cvut.cz/~mptp/nn_conj20/results/preddatagpt1.out.tar.gz)
4. Siemion Fajtlowicz. On conjectures of Graffiti. Annals of Discrete Mathematics, 72(1–3):113–118, 1988. [find](https://scholar.google.com/scholar?q=Siemion+Fajtlowicz%2E+On+conjectures+of+Graffiti%2E+Annals+of+Discrete+Mathematics%2C+72%281%E2%80%933%29%3A113%E2%80%93118%2C+1988%2E)
5. Thibault Gauthier. Deep reinforcement learning in HOL4. CoRR, abs/1910.[11797, 2019](https://md.research.elamur.ai/free/en/papers/gauthier-2019-deep-reinforcement-learning-synthesizing-functions/).
6. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Initial experiments with statistical conjecturing over large formal corpora. In CICM’16 WiP Proceedings, pages 219–228, 2016. [find](https://scholar.google.com/scholar?q=Thibault+Gauthier%2C+Cezary+Kaliszyk%2C+and+Josef+Urban%2E+Initial+experiments+with+statistical+conjecturing+over+large+formal+corpora%2E+In+CICM%E2%80%9916+WiP+Proceedings%2C+pages+219%E2%80%93228%2C+2016%2E)
7. Moa Johansson, Dan Rosén, Nicholas Smallbone, and Koen Claessen. Hipster: Integrating theory exploration in a proof assistant. In CICM 2014, pages 108–122, 2014. [find](https://scholar.google.com/scholar?q=Moa+Johansson%2C+Dan+Rose%CC%81n%2C+Nicholas+Smallbone%2C+and+Koen+Claessen%2E+Hipster%3A+Integrating+theory+exploration+in+a+proof+assistant%2E+In+CICM+2014%2C+pages+108%E2%80%93122%2C+2014%2E)
8. Cezary Kaliszyk, Josef Urban, and Jirı́ Vyskocil. Automating formalization by statistical and semantic parsing of mathematics. In ITP, pages 12–27, 2017. [find](https://scholar.google.com/scholar?q=Cezary+Kaliszyk%2C+Josef+Urban%2C+and+Jir%C4%B1%CC%81+Vyskocil%2E+Automating+formalization+by+statistical+and+semantic+parsing+of+mathematics%2E+In+ITP%2C+pages+12%E2%80%9327%2C+2017%2E)
9. Cezary Kaliszyk, Josef Urban, and Jiřı́ Vyskočil. Learning to parse on aligned corpora (rough diamond). In ITP 2015, pages 227–233, 2015. [find](https://scholar.google.com/scholar?q=Cezary+Kaliszyk%2C+Josef+Urban%2C+and+Jir%CC%8C%C4%B1%CC%81+Vyskoc%CC%8Cil%2E+Learning+to+parse+on+aligned+corpora+%28rough+diamond%29%2E+In+ITP+2015%2C+pages+227%E2%80%93233%2C+2015%2E)
10. Douglas Bruce Lenat. AM: An Artificial Intelligence Approach to Discovery in Mathematics as Heuristic Search. PhD thesis, Stanford, 1976. [find](https://scholar.google.com/scholar?q=Douglas+Bruce+Lenat%2E+AM%3A+An+Artificial+Intelligence+Approach+to+Discovery+in+Mathematics+as+Heuristic+Search%2E+PhD+thesis%2C+Stanford%2C+1976%2E)
11. Bartosz Piotrowski and Josef Urban. [Stateful premise selection by recurrent neural networks](https://md.research.elamur.ai/free/en/papers/piotrowski-2020-stateful-premise-selection-recurrent-neural/), 2020.
12. Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. Language models are unsupervised multitask learners. OpenAI Blog, 1(8):9, 2019. [find](https://scholar.google.com/scholar?q=Alec+Radford%2C+Jeffrey+Wu%2C+Rewon+Child%2C+David+Luan%2C+Dario+Amodei%2C+and+Ilya+Sutskever%2E+Language+models+are+unsupervised+multitask+learners%2E+OpenAI+Blog%2C+1%288%29%3A9%2C+2019%2E)
13. Stephan Schulz. System description: E 1.8. In Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov, editors, LPAR, volume 8312 of LNCS, pages 735–743. Springer, 2013. [find](https://scholar.google.com/scholar?q=Stephan+Schulz%2E+System+description%3A+E+1%2E8%2E+In+Kenneth+L%2E+McMillan%2C+Aart+Middeldorp%2C+and+Andrei+Voronkov%2C+editors%2C+LPAR%2C+volume+8312+of+LNCS%2C+pages+735%E2%80%93743%2E+Springer%2C+2013%2E)
14. Josef Urban. XML-izing Mizar: Making semantic processing and presentation of MML easy. In Michael Kohlhase, editor, MKM, volume 3863 of LNCS, pages 346–360. Springer, 2005. [find](https://scholar.google.com/scholar?q=Josef+Urban%2E+XML%2Dizing+Mizar%3A+Making+semantic+processing+and+presentation+of+MML+easy%2E+In+Michael+Kohlhase%2C+editor%2C+MKM%2C+volume+3863+of+LNCS%2C+pages+346%E2%80%93360%2E+Springer%2C+2005%2E)
15. Josef Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21–43, 2006. [find](https://scholar.google.com/scholar?q=Josef+Urban%2E+MPTP+0%2E2%3A+Design%2C+implementation%2C+and+initial+experiments%2E+J%2E+Autom%2E+Reasoning%2C+37%281%2D2%29%3A21%E2%80%9343%2C+2006%2E)
16. Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, and Josef Urban. [Exploration of neural machine translation in autoformalization of mathematics in mizar](https://md.research.elamur.ai/free/en/papers/wang-2019-exploration-neural-machine-translation-autoformalization/). In CPP, pages 85–98, 2020.
17. Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. [First experiments with neural translation of informal to formal mathematics](https://md.research.elamur.ai/free/en/papers/wang-2018-first-experiments-neural-translation-informal/). In CICM, pages 255–270, 2018.

*Updated 3 November 2026*