Compfiles: Catalog Of Math Problems Formalized In Lean

Since 1972, the USA Mathematical Olympiad has included a total of 294 problems.

38 problems have been formalized (12.92%).

25 problems have complete formalized solutions (8.50%).

2024P1P2P3P4P5P6
2023P1P2P3P4P5P6
2022P1P2P3P4P5P6
2021P1P2P3P4P5P6
2020P1P2P3P4P5P6
2019P1P2P3P4P5P6
2018P1P2P3P4P5P6
2017P1P2P3P4P5P6
2016P1P2P3P4P5P6
2015P1P2P3P4P5P6
2014P1P2P3P4P5P6
2013P1P2P3P4P5P6
2012P1P2P3P4P5P6
2011P1P2P3P4P5P6
2010P1P2P3P4P5P6
2009P1P2P3P4P5P6
2008P1P2P3P4P5P6
2007P1P2P3P4P5P6
2006P1P2P3P4P5P6
2005P1P2P3P4P5P6
2004P1P2P3P4P5P6
2003P1P2P3P4P5P6
2002P1P2P3P4P5P6
2001P1P2P3P4P5P6
2000P1P2P3P4P5P6
1999P1P2P3P4P5P6
1998P1P2P3P4P5P6
1997P1P2P3P4P5P6
1996P1P2P3P4P5P6
1995P1P2P3P4P5
1994P1P2P3P4P5
1993P1P2P3P4P5
1992P1P2P3P4P5
1991P1P2P3P4P5
1990P1P2P3P4P5
1989P1P2P3P4P5
1988P1P2P3P4P5
1987P1P2P3P4P5
1986P1P2P3P4P5
1985P1P2P3P4P5
1984P1P2P3P4P5
1983P1P2P3P4P5
1982P1P2P3P4P5
1981P1P2P3P4P5
1980P1P2P3P4P5
1979P1P2P3P4P5
1978P1P2P3P4P5
1977P1P2P3P4P5
1976P1P2P3P4P5
1975P1P2P3P4P5
1974P1P2P3P4P5
1973P1P2P3P4P5
1972P1P2P3P4P5