JohnYang88/lean-dojo-mathlib4
收藏Hugging Face2023-12-11 更新2024-03-04 收录
下载链接：
https://hf-mirror.com/datasets/JohnYang88/lean-dojo-mathlib4
下载链接
链接失效反馈官方服务：
资源简介：
lean-dojo-mathlib4 数据集
lean-dojo-mathlib4 数据集
提供机构：
JohnYang88
原始信息汇总
数据集概述
数据集信息
特征
- url: 字符串类型
- commit: 字符串类型
- file_path: 字符串类型
- full_name: 字符串类型
- start: 整数类型
- end: 整数类型
- traced_tactics: 字符串类型
分割
- train:
- 字节数: 320023872
- 样本数: 98514
- test:
- 字节数: 6116916
- 样本数: 2000
- validation:
- 字节数: 7228697
- 样本数: 2000
大小
- 下载大小: 54194769
- 数据集大小: 333369485
配置
- default:
- 训练数据路径: data/train-*
- 测试数据路径: data/test-*
- 验证数据路径: data/validation-*
