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, 205 problems and 125 solutions have been formalized.

TotalFormalizedSolved
IMO39214078
USAMO2944229
FormalizedSolved
Algebra10576
Number Theory6336
Combinatorics2910
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.