We present FIMO, an innovative dataset comprising formal mathematical problem statements sourced from the International Mathematical Olympiad (IMO) Shortlisted Problems. Designed to facilitate advanced automated theorem proving at the IMO level, FIMO is currently tailored for the Lean formal language. It comprises 149 formal problem statements, accompanied by both informal problem descriptions and their corresponding LaTeX-based informal proofs. Through initial experiments involving GPT-4, our findings underscore the existing limitations in current methodologies, indicating a substantial journey ahead before achieving satisfactory IMO-level automated theorem proving outcomes.

翻译：我们提出了FIMO，这是一个创新性数据集，包含源自国际数学奥林匹克竞赛（IMO）预选题的形式化数学问题陈述。该数据集旨在促进IMO级别的先进自动化定理证明，目前专门针对Lean形式化语言进行了适配。数据集包含149个形式化问题陈述，并附有非形式化问题描述及其基于LaTeX的非形式化证明。通过使用GPT-4进行的初步实验，我们的研究结果突显了现有方法的局限性，表明在实现令人满意的IMO级别自动化定理证明结果之前，仍有漫长的探索之路。