Compfiles: Catalog Of Math Problems Formalized In Lean

Welcome to Compfiles, a collaborative repository of olympiad-style math problems that have been formalized in the Lean theorem prover.

So far, 202 problems and 117 solutions have been formalized.

TotalFormalizedSolved
IMO39213772
USAMO2944227
FormalizedSolved
Algebra10372
Number Theory6333
Combinatorics289
Geometry72

Frequently Asked Questions

Why are you doing this?

Why is Compfiles a separate project when Mathlib/Archive/Imo already exists?

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.

How does Compfiles compare to MiniF2F?

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.

How does Compfiles encode problems that ask for data values to be determined?

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.

I noticed an error on this website. How do I report it?

Please open an issue on Github.