Formalizing IMO Problems and Solutions in Isabelle/HOL
Filip Mari\'c (Faculty of Mathematics, University of Belgrade,, Serbia), Sana Stojanovi\'c-{\Dj}ur{\dj}evi\'c (Faculty of Mathematics,, University of Belgrade, Serbia)
TL;DR
This paper introduces a project to formalize IMO problems and solutions in Isabelle/HOL, aiming to advance AI capabilities in solving complex mathematical competitions by creating a verified repository of solutions.
Contribution
It presents an initial step towards formalizing IMO problems in Isabelle/HOL, contributing a maintained repository of mechanically checked solutions to support AI research.
Findings
Created a repository of formalized IMO solutions in Isabelle/HOL
Engaged students in formalizing mathematical problems and solutions
Lays groundwork for AI systems to solve IMO problems
Abstract
The International Mathematical Olympiad (IMO) is perhaps the most celebrated mental competition in the world and as such is among the greatest grand challenges for Artificial Intelligence (AI). The IMO Grand Challenge, recently formulated, requires to build an AI that can win a gold medal in the competition. We present some initial steps that could help to tackle this goal by creating a public repository of mechanically checked solutions of IMO Problems in the interactive theorem prover Isabelle/HOL. This repository is actively maintained by students of the Faculty of Mathematics, University of Belgrade, Serbia within the course "Introduction to Interactive Theorem Proving".
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.