adeo1/mathlib_informal_v4.24.0

该数据集包含Lean v4.24.0 mathlib声明及其非正式描述，由Autoprover丰富管道生成，并采用检索模式发布。数据集以JSONL格式存储，每个声明对应一个JSON对象，包含189,937个训练样本。特征包括文档ID、全名、短名、模块名、文件路径、类型、签名、文档字符串、形式化陈述、非正式化陈述、非正式名称、形式化搜索文本、非正式化搜索文本、联合搜索文本、依赖名称序列、导入模块名称序列、重要性评分和来源语料。数据集已进行清理和规范化处理，如去除机器本地路径、将文件路径规范化为Mathlib/...、来源语料规范化为Mathlib，并将文档ID规范化为<文件路径>:<全名>。数据集适用于文本检索任务，支持英语和代码语言，大小为100K到1M之间，许可证为MIT。

This dataset contains Lean v4.24.0 mathlib declarations with informal descriptions produced by the Autoprover enrichment pipeline and published in the retrieval schema used by this codebase. The dataset is stored in JSONL format with one JSON object per declaration, containing 189,937 training examples. Features include doc_id, full_name, short_name, module_name, file_path, kind, signature, docstring, formal_statement, informal_statement, informal_name, search_text_formal, search_text_informal, search_text_joint, dependency_names sequence, imported_module_names sequence, importance_score, and source_corpus. The dataset has been cleaned and normalized, such as removing machine-local paths, normalizing file_path to Mathlib/..., source_corpus to Mathlib, and doc_id to <file_path>:<full_name>. It is suitable for text retrieval tasks, supports English and code languages, has a size category between 100K and 1M, and is licensed under MIT.