A collection of olympiad-style math problems and their solutions, formalized in Lean 4.

Some problems were imported from external sources:

• mathlib4/Archive/Imo.
• Gian Sanjaya's Lean 3 and Lean 4 formalizations of IMO shortlist problems.

A list of all the problems and their status is available as a dashboard that gets automatically updated on every push to the main branch of this repo.

Make sure you have elan installed. Then do:

$ lake exe cache get
$ lake build

In this repo, each solution (proof) is recorded inline, in the same file that its problem is declared. In some situations, however, solution data is undesired. For example, we might want a website to display only the problem statement, or we might want to invoke an IMO Grand Challenge solver without providing spoilers.

To that end, this repo defines some special commands to support problem extraction.

• A problem_file command marks a file that should participate in problem extraction.
• A problem declaration is the main theorem to be proved. The body of the declaration (everything to the right of :=) is replaced by sorry in the extracted problem.
• A determine declaration indicates data the must be provided as part of the solution. Like with problem, the body of the declaration is replaced by sorry in the extracted problem.
• A snip begin ... snip end sequence indicates commands that should be omitted in the extracted problem.

To generate problem statements with all solution information stripped, do:

$ lake exe extractProblems

and then look in the _extracted/problems directory.

Sometimes it's useful to have a version of a solution that does not depend on the ProblemExtraction library (but still contains all proof information). For example, you might want to share a fully worked solution on https://live.lean-lang.org/.

To that end, the extractProblems tool described above additionally extracts dependency-stripped solution files into the _extracted/solutions directory.

The checkSolution executable takes as input a problem ID and a path to a lean source code file. For example:

$ lake exe checkSolution Imo2022P2 _extracted/solutions/Imo2022P2.lean

This will check that the extracted solution file _extracted/solutions/Imo2022P2.lean does indeed pass verification for problem Imo2022P2. It will print the terms for any determine declarations in the solution, so that they can be judged by a human. In this example, that will look like:

determine Imo2022P2.solution_set := {fun x => 1 / x}

The intention is that this solution checker could be used as a grader for the IMO Grand Challenge.

Contributions are welcome! You may take credit for you work by adding yourself to the "authors" field in the copyright header.

IMO 1964 Problem 4
IMO 1964 Problem 1b