Dataset Groups Activity Stream 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. BibTex: @dataset{Cezary_Kaliszyk_and_Josef_Urban_2024, abstract = {The dataset consists of the core HOL Light corpus and the Flyspeck corpus, with millions of nodes representing atomic inferences.}, author = {Cezary Kaliszyk and Josef Urban}, doi = {10.57702/k3dte6ep}, institution = {No Organization}, keyword = {'Flyspeck', 'Formal verification', 'HOL Light', 'Mathematics'}, month = {dec}, publisher = {TIB}, title = {HOL Light and Flyspeck corpora}, url = {https://service.tib.eu/ldmservice/dataset/hol-light-and-flyspeck-corpora}, year = {2024} }
