phanerozoic/Coq-MetaCoq-QA

MetaCoq Q&A数据集是MetaCoq数据集的对话扩展，源自Coq元理论的MetaCoq形式化。该数据集将元理论内容转化为结构化的问答对，通过自然语言交互使形式化元编程和验证概念更易于理解。每个条目代表一个从MetaCoq中提取的数学陈述（定义、定理、引理等），并转换为自然语言的问答格式，同时保留了原始的元理论上下文和特定的MetaCoq构造（如Quote Definition和MetaCoq Run）。该数据集基于原始的MetaCoq数据集和Coq-HoTT Q&A数据集的方法构建。The MetaCoq Q&A Dataset is a conversational extension of the MetaCoq Dataset, derived from the MetaCoq formalization of Coqs 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, theorem, lemma, etc.) converted into a natural language question-answer format while preserving the original meta-theoretical context and specific MetaCoq constructs like Quote Definition and MetaCoq Run. The dataset includes the following fields: question, answer, and context, and covers major MetaCoq directories. The dataset is designed for use in conversational AI, meta-programming education, formal methods research, and documentation generation. The dataset is licensed under the MIT license.