## 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.

| Total | Formalized | Solved |
---|

IMO | 392 | 137 | 71 |
---|

USAMO | 294 | 42 | 28 |
---|

| Formalized | Solved |
---|

Algebra | 103 | 71 |
---|

Number Theory | 63 | 34 |
---|

Combinatorics | 28 | 9 |
---|

Geometry | 7 | 2 |
---|

### 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.