MiniF2F

该数据集名为miniF2F，包含488个来自高中竞赛的正式数学问题，这些问题以三种形式化语言表达：Lean、HOL-Light和Isabelle。数据集涵盖了三个类别的问题：260个来自MATH数据集，160个来自实际高中竞赛，以及68个为匹配前述竞赛难度而设计的问题。总共有488个问题，其中验证集和测试集各有244个。任务是对miniF2F数据集中的问题生成形式化的草图。

The miniF2F dataset consists of 488 formal mathematical problems related to high school competitions, which are represented in three formal languages: Lean, HOL-Light, and Isabelle. The dataset covers three categories of problems: 260 sourced from the MATH dataset, 160 from real high school competitions, and 68 problems designed to match the difficulty level of the aforementioned competitions. In total, there are 488 problems, with 244 allocated to the validation set and another 244 to the test set. The task is to generate formal sketches for the problems in the miniF2F dataset.