FIMO: A Challenge Formal Dataset for Automated Theorem Proving

Understand

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.