The goal of this project is to formalize one of these problems, together with its solution, in the interactive proof assistant Isabelle. Isabelle is a software tool that allows mathematical concepts to be defined in a formal language, that offers tools to construct proofs of mathematical theorems in a logical calculus, and that checks these proofs to ensure their correctness. This makes formal, machine-checked proofs far more reliable than traditional pen-and-paper proofs.
In other words, the challenge is not to solve one of the IMO problems, but rather to formalize one of the (known) solutions in Isabelle. How difficult will it be to construct a formal proof? How much interaction will be required; will Isabelle be able to find parts of the proof automatically? Are basic definitions and lemmas already present in Isabelle's libraries, or will they need to be added? How much longer than the pen-and-paper solution will the formal proof be? These are the interesting questions that this project aims to answer.
This project will allow you to become familiar with Isabelle, one of the world's leading software tools to assist with the development of formal proofs.