datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
news-categoriesagda-categories-informalized
agda-categories, informalized
4,541 declarations from the agda-categories
library, each paired with an informal, LaTeX-flavoured natural-language
statement written by GLM-5.2. The natural language is written to be precise
enough to re-formalise from, so the intended use is training a model to
reconstruct the formal Agda source from the prose alone.
Declarations were extracted with a fork of Agda
that dumps one JSON record per named declaration (with its full source range)
during… See the full description on the dataset page: https://huggingface.co/datasets/astral-expmath/agda-categories-informalized.Agda-Categories
Agda-Categories
Structured dataset from agda-categories — Category theory.
Source
Repository: https://github.com/agda/agda-categories
Commit: fbd1259c2dcf011ee1936fa8c24a1b10e6285673
Files: 521
License: mit
Schema
Column
Type
Description
statement
string
Declaration signature/claim with the leading keyword removed (verbatim slice); the full declaration minus its proof
proof
string
Verbatim proof/body, empty if the declaration has none… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Agda-Categories.