phanerozoic/Coq-UniMath

UniMath数据集源自UniMath仓库，专注于在Coq证明助手中形式化Univalent Mathematics。该数据集处理核心数学库中的.v文件，以结构化格式提取数学内容。数据集包括数学陈述、类型、来源库、导入语句、源文件路径等字段。数据集适用于形式方法研究、机器学习应用、教育目的和数学分析。数据集遵循BSD 2-clause许可。

The UniMath Dataset is derived from the UniMath repository, focusing on the formalization of Univalent Mathematics in the Coq proof assistant. This dataset processes .v files from the core mathematical libraries to extract mathematical content in a structured format. The dataset includes fields such as mathematical statement body, statement type, originating library, Require Import statements, source file path, mathematical object identifier, and sequential index for the dataset. It covers content from various UniMath libraries including Algebra, CategoryTheory, Foundations, and more, and is designed for formal methods research, machine learning applications, educational purposes, and mathematical analysis.