mathcontest-lean

mathcontest-lean is a collection of formalized mathematics olympiad problems written in Lean 4. The goal of this project is to rigorously verify solutions to contest problems.

🔧 Structure

• OKTV/ — Problems from the Hungarian National Secondary School Academic Competition
• AranyDaniel/ — Problems from the Dániel Arany Secondary School Mathematics Competition

▶️ Trying It Out

You can try out the proofs directly in your browser using the Lean 4 Web Editor.
Just copy and paste the Lean code from this repository into the editor — no installation required.

❗ Mistakes in Official Solutions

Sometimes even official solutions contain subtle mistakes. This section tracks such discoveries made during formalization.

Problem	Official Solution	Mistake
OKTV2006_I_II_P5	oktatas.hu	The official solution doesn't check whether p = 19 after determining that 7 < p < 21. Fortunately, this doesn't affect the final result.

✅ List of formalized problems

Problem	Solved	Topics
OKTV2024_II_I_P4	✅	number theory
OKTV2023_I_II_P3	✅	algebra
OKTV2024_I_II_P3	✅	functions
OKTV2024_III_I_P3	✅	functions
OKTV2024_II_II_P4	✅	functions
OKTV2014_II_I_P3	✅	functions
OKTV2020_I_II_P2	✅	functions
OKTV2015_I_II_P3	✅	inequalities, trigonometry
OKTV2020_III_I_P5	✅	functions
OKTV2016_III_I_P3	✅	algebra, trigonometry
OKTV2019_III_I_P3	✅	algebra
OKTV2009_I_II_P4	❌	inequalities
OKTV2011_I_I_P1	✅	algebra
OKTV2012_I_II_P1	✅	algebra
OKTV2017_I_I_P2	✅	algebra
OKTV2018_I_III_P1	❌	number theory
OKTV2018_I_II_P4	✅	algebra
OKTV2019_I_II_P3	✅	algebra
OKTV2019_I_I_P5	✅	algebra
OKTV2020_I_II_P1	✅	algebra
OKTV2016_II_II_P2	❌	inequalities
OKTV2009_II_III_P1	❌	inequalities
OKTV2012_II_I_P1	✅	algebra
OKTV2017_II_I_P3	✅	algebra
OKTV2015_II_I_P3	✅	number theory
OKTV2014_I_I_P4	✅	algebra
OKTV2014_III_I_P1	✅	number theory
OKTV2024_I_I_P3	✅	algebra
OKTV2009_II_I_P3	✅	algebra
OKTV2011_II_I_P1	✅	algebra
OKTV2018_II_I_P2	✅	inequalities
OKTV2019_III_I_P1	❌	number theory
OKTV2004_I_I_P3	✅	number theory
OKTV2004_I_I_P4	✅	number theory
OKTV2010_III_I_P3	✅	number theory
OKTV2010_II_I_P3	✅	inequalities
OKTV2018_II_I_P5	❌	number theory
OKTV2020_II_III_P1	✅	inequalities
OKTV2015_II_II_P4	✅	number theory
OKTV2016_II_I_P4	✅	number theory
OKTV2016_III_III_P3	❌	number theory
OKTV2020_III_I_P1	✅	number theory
OKTV2022_I_I_P1	✅	number theory
OKTV2023_II_I_P4	✅	number theory
OKTV2013_I_I_P1	✅	algebra
OKTV2013_I_I_P2	✅	number theory
OKTV2006_I_II_P5	✅	number theory
OKTV2010_I_I_P4	✅	number theory
OKTV2014_I_I_P3	✅	number theory
OKTV2011_III_I_P3	✅	number theory
OKTV2018_III_I_P2	✅	number theory
OKTV2007_II_I_P3	✅	number theory
OKTV2019_II_II_P3	✅	number theory
OKTV2016_II_II_P3	✅	number theory
OKTV2021_II_II_P1	✅	number theory
OKTV2022_II_II_P4	✅	number theory
Arany2018_B_III_II_P2	✅	functions
Arany2012_A_I_I_P3	✅	number theory
Arany2019_A_III_II_P2	✅	inequalities
Arany2015_B_III_II_P1	✅	number theory
Arany1998_B_I_I_P3	✅	algebra
Arany1998_B_I_I_P1	✅	number theory
Arany2021_A_II_II_P2	❌	algebra
Arany2015_B_II_III_P1	✅	number theory
Arany2014_A_II_I_P3	✅	number theory
Arany2012_A_II_III_P3	✅	number theory
Arany2012_B_II_III_P3	❌	algebra, number theory
Arany2011_A_II_II_P1	✅	algebra, number theory
Arany2011_A_I_I_P4	✅	number theory
Arany2011_B_I_I_P3	✅	number theory
Arany2013_A_II_II_P3	✅	number theory
Arany2013_B_II_III_P3	✅	number theory
Arany2013_A_I_II_P2	✅	number theory
Arany2014_B_I_II_P2	✅	inequalities
Arany2014_B_I_I_P2	✅	number theory
Arany2015_A_I_I_P5	✅	algebra
Arany2016_A_II_III_P3	✅	algebra
Arany2016_A_II_II_P1	✅	number theory
Arany2015_A_I_II_P1	✅	inequalities, number theory
Arany2018_A_III_I_P2	✅	number theory
Arany2020_A_I_I_P1	✅	number theory
Arany2020_B_I_II_P1	✅	number theory
Arany2021_A_III_I_P1	✅	algebra
Arany2021_B_I_III_P1	❌	number theory
Arany2022_A_II_III_P1	❌	number theory
Arany2022_A_III_II_P1	✅	number theory
Arany2022_A_III_I_P3	✅	number theory
Arany2022_B_I_I_P3	✅	number theory
Arany2023_A_III_I_P2	✅	number theory
Arany2023_A_I_II_P1	✅	algebra, number theory
Arany2023_A_II_I_P2	✅	number theory
Arany2023_A_I_I_P3	✅	algebra
Arany2023_A_I_I_P1	✅	number theory
Arany2023_B_III_I_P2	✅	algebra, inequalities