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）候选问题的形式化数学问题陈述。FIMO旨在促进IMO级别的先进自动化定理证明，目前专为Lean形式化语言定制。该数据集包含149个形式化问题陈述，并附有非正式问题描述及其对应的基于LaTeX的非形式化证明。通过涉及GPT-4的初步实验，我们的发现凸显了当前方法的局限性，表明在实现令人满意的IMO级别自动化定理证明结果之前，仍有漫长的征程。