Formalizing Problems and Solutions from the 2023 International Mathematical Olympiad

The International Mathematical Olympiad is a highly prestigious annual mathematical competition for high-school students. IMO2023, the 64th edition of this competition, took place from July 2 to July 13 in Chiba, Japan. Over sixhundred paticipants competed on six challenging mathematical problems covering topics such as algebra, combinatorics, geometry and number theory.

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.

Work environment:
Isabelle (Windows/macOS/Linux)
Useful knowledge/skills:
Basic mathematics, first-order logic
Tjark Weber

Last modified: 2023-11-05