IMO-Prover/LeanWorkbook-filtered
收藏Hugging Face2025-04-11 更新2025-04-12 收录
下载链接：
https://hf-mirror.com/datasets/IMO-Prover/LeanWorkbook-filtered
下载链接
链接失效反馈官方服务：
资源简介：
该数据集包含问题ID、非正式描述、正式描述和领域四个字段，适用于训练自然语言处理模型。数据集分为训练集，共有40076个示例，数据大小为14449278字节。
The dataset includes problem ID, informal statement, formal statement, and domain fields, suitable for training natural language processing models. The dataset is split into a training set with a total of 40,076 examples, with a data size of 14,449,278 bytes.
提供机构：
IMO-Prover
