Welcome to Compfiles, a collaborative repository of olympiad-style math problems that have been formalized in the Lean theorem prover.
So far, 205 problems and 125 solutions have been formalized.
Total | Formalized | Solved | |
---|---|---|---|
IMO | 392 | 140 | 78 |
USAMO | 294 | 42 | 29 |
Formalized | Solved | |
---|---|---|
Algebra | 105 | 76 |
Number Theory | 63 | 36 |
Combinatorics | 29 | 10 |
Geometry | 7 | 2 |
We want to minimize the burden that we place on Mathlib's maintainers and infrastructure. Mathlib is a large enough monolith already. Since Mathlib and Compfiles are both open source under the Apache-2.0 license, it should be straightforward to move code back and forth between them, if desired.
MiniF2F is a static benchmark for machine learning, with 488 math problems formalized in multiple languages (Lean, Metamath, Isabelle, and HOL Light) including a relatively small number of formalized solutions. Compfiles is a continually-growing archive of math problems formalized in Lean, with emphasis placed on complete formalized solutions.
We have special determine
command to mark such data. You can see it in action for Imo2015P5 in the source code and on the rendered webpage, and you can see its definition here.
Please open an issue on Github.