A collection of olympiad-style math problems and their solutions, formalized in Lean 4.
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_filecommand marks a file that should participate in problem extraction. - A
problemdeclaration is the main theorem to be proved. The body of the declaration (everything to the right of:=) is replaced bysorryin the extracted problem. - A
determinedeclaration indicates data the must be provided as part of the solution. Like withproblem, the body of the declaration is replaced bysorryin the extracted problem. - A
snip begin...snip endsequence 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.
Some problems were imported from external sources:
- mathlib4/Archive/Imo.
- Gian Sanjaya's Lean 3 and Lean 4 formalizations of IMO shortlist problems.
| IMO 1987 Problem 4 |  |
| IMO 1964 Problem 4 |  |
| IMO 1964 Problem 1b |  |
