miniF2F

miniF2F是一个针对形式化奥林匹克数学问题的数据集，旨在为神经定理证明提供一个统一的跨系统基准。该数据集包含488个问题陈述，来源于AIME、AMC和国际数学奥林匹克（IMO）等，以及高中和本科数学课程的材料。数据集的创建过程涉及手动形式化，覆盖了多种难度级别，适用于人类和机器。miniF2F的应用领域主要集中在推动神经定理证明技术的发展，解决形式化数学推理的高难度问题。

miniF2F is a dataset focused on formalized Olympiad mathematics problems, aiming to provide a unified cross-system benchmark for neural theorem proving. This dataset contains 488 problem statements sourced from competitions such as AIME, AMC, and the International Mathematical Olympiad (IMO), as well as teaching materials from high school and undergraduate mathematics curricula. The dataset was constructed via manual formalization, spans multiple difficulty levels, and is suitable for both humans and machines. The core application scenarios of miniF2F center on advancing the development of neural theorem proving technologies and solving challenging problems in formal mathematical reasoning.