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

Frequently Asked Questions

Why are you doing this?

• It's a fun way to learn about math and mechanized reasoning!
• It uncovers missing pieces of theory that ought to be in Mathlib. See for example Joseph Myers's Euclidean geometry TODO list.
• It's a (small) first step toward solving the IMO Grand Challenge.

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.