HOL Light and Flyspeck corpora

The dataset consists of the core HOL Light corpus and the Flyspeck corpus, with millions of nodes representing atomic inferences.

Data and Resources

Original MetadataJSON
The json representation of the dataset with its distributions based on DCAT.
Explore
- Preview
- Download

Cezary Kaliszyk, Josef Urban (2024). Dataset: HOL Light and Flyspeck corpora. https://doi.org/10.57702/k3dte6ep

DOI retrieved: December 3, 2024

Field	Value
Created	December 3, 2024
Last update	December 3, 2024
Defined In	https://doi.org/10.48550/arXiv.1310.2797
Author	Cezary Kaliszyk
More Authors	Josef Urban
Homepage	http://mizar.cs.ualberta.ca/~mptp/lemma_mining/