JohnYang88/lean-dojo-mathlib4

lean-dojo-mathlib4 数据集lean-dojo-mathlib4 数据集

原始信息汇总

数据集概述

数据集信息

特征

• 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-*