IMOSLLean4

Formalization of IMO Shortlist Problems in Lean 4.

This repository stores formalization of IMO Shortlist problems from 2006 onwards in Lean 4. It mainly covers problems in the Algebra and Number Theory category, with some problems in the Combinatorics category included as well. All problems formalized here include their complete solutions.

Aside from formalizing the IMO Shortlist problems, this repository also formalizes attempts to generalize a few of these problems. For example, after rephrasing, the IMO Shortlist 2012 N8 problem reads as follows.

For any prime power , let be the finite field of elements. Prove that for every prime and for every , there exist two elements such that .

Then we prove more:

For any finite field of cardinality not equal to and for every , there exist two elements such that (and that this fails for cardinality ).

Installation and Dependencies

Please follow the instructions at https://leanprover-community.github.io/install/project.html about working on an existing project.

This project depends on Mathlib4 and is currently using version 4.28.0.

Documentation

The documentation of this project is available on this webpage. This documentation is built using doc-gen4.

The folder IMOSLLean4/Main contains the formalization of the IMO Shortlist problems. The files here are organized by year. The formalization of the main statement to be proved is named final_solution. If there are multiple parts to the problem, then part 1 is named final_solution_part1, part 2 is named final_solution_part2, and so on.

Meanwhile, the folder IMOSLLean4/Generalization contains formalization of generalized versions of some IMO Shortlist problems, such as the aforementioned IMO Shortlist 2012 N8 problem. The files here are organized by the problem they generalize.

Contributing

Thank you for your interest in contributing to this project! This repository is a personal project, so currently I am not looking for external contributions. That being said, feel free to fork this repository for your needs.

Progress

Below are some statistics on the number of problems formalized in this repository as of March 11, 2026. Here, "A" stands for Algebra, "C" stands for Combinatorics, and "N" stands for Number Theory.