datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
Coq-Changelog-QA
Coq Changelog Q&A Dataset
Dataset Description
The Coq Changelog Q&A Dataset is an extension of the original Coq Changelog Dataset, transforming each changelog entry into two Question–Answer pairs via two distinct prompts. One focuses on a straightforward query about the change itself, while the other aims at the rationale or motivation behind it. By applying both prompts to every changelog entry, the dataset approximately doubles in size compared to the source.… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Coq-Changelog-QA.Coq-HoTT-QA
Coq-HoTT Q&A Dataset
Dataset Description
The Coq-HoTT Q&A Dataset is a conversational extension of the Coq-HoTT Dataset, derived directly from the Coq-HoTT GitHub repository (https://github.com/HoTT/Coq-HoTT). This dataset transforms Homotopy Type Theory (HoTT) content into structured Q&A pairs, bridging the gap between formal mathematics and conversational AI.
Each entry in the dataset represents a mathematical statement, such as a definition or theorem, converted into a… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Coq-HoTT-QA.Coq-UniMath-QA
UniMath Q&A Dataset
Dataset Description
The UniMath Q&A Dataset is a conversational extension of the UniMath Dataset, derived from the UniMath formalization of mathematics (https://github.com/UniMath/UniMath). This dataset transforms Univalent Mathematics content into structured Q&A pairs, making formal mathematical content more accessible through natural language interactions.
Each entry represents a mathematical statement from UniMath (definition, theorem, lemma, etc.)… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Coq-UniMath-QA.Coq-MetaCoq-QA
MetaCoq Q&A Dataset
Dataset Description
The MetaCoq Q&A Dataset is a conversational extension of the MetaCoq Dataset, derived from the MetaCoq formalization of Coq's meta-theory (https://github.com/MetaCoq/metacoq). This dataset transforms meta-theoretical content into structured Q&A pairs, making formal meta-programming and verification concepts more accessible through natural language interactions.
Each entry represents a mathematical statement from MetaCoq (definition… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Coq-MetaCoq-QA.