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

TotalFormalizedSolved
IMO38610761
USAMO2943824
FormalizedSolved
Algebra8159
Number Theory5329
Combinatorics248
Geometry62