AI4Math ChronicleAI4Math 大事记

miniF2F 建立跨形式系统的奥赛数学基准

该基准把 AIME、AMC、IMO 及教学来源中的问题翻译为形式语言。其贡献不是新的数学定理，而是为学习式定理证明器提供可复现、可训练和可比较的共同目标。

发生了什么？

miniF2F 引入了 488 个形式化的奥赛级数学题目陈述，覆盖 Metamath、Lean 等证明助手，并提供用于跨系统定理证明评测的留出划分。

为什么重要？

miniF2F 成为形式化 AI4Math 的核心评测基础之一，使 LeanDojo、COPRA、DeepSeek-Prover 等后续系统能够在一个可识别的共享任务上报告进展。

重要性说明：miniF2F 将奥赛级题目整理为多个形式系统中的共享题集，使神经定理证明方法更容易直接比较，并成为后来多种 Lean 证明器长期使用的评测目标。

历史脉络

更早进展
后续进展
相关里程碑

—

主要证据

证据与状态一览

重要性
H2 · 领域里程碑
验证状态
论文已发布
证据等级
E3 · 可检查工件
AI 角色
仅计算支持
形式保障
有形式化工件

如何理解这些标签？ →

贡献与验证

数学新颖性
工具性进展
接口
形式化, 符号
AI 贡献
AI 系统在该数据集上接受评测，但基准构建与形式化题目整理主要由人类完成，并非 AI 数学发现事件。
人类贡献
作者选择原始问题、翻译并整理形式化陈述、设计评测划分，并维护跨系统评测资源。
验证状态
论文已发布 · E3 · 可检查工件 · 有形式化工件
最后审阅
2026-09-11

技术细节

系统
minif2f, lean, metamath, isabelle, hol-light
机构
openai, formal-mathematics-community
数学问题
olympiad-mathematics
方法
benchmarking, formalization, theorem-proving

全部来源与工件

验证历史

  • 2021-08-31 · 论文已发布 · E2 · 研究记录

    该基准通过 arXiv 论文公开说明，并以形式数学公共仓库的形式发布。

更正

当前没有记录的更正。