Solving (Some) Formal Math Olympiad Problems

We built a neural theorem prover for Lean [https://leanprover.github.io/] that learned to solve a variety of challenging high-school olympiad problems, including problems from the AMC12 [https://www.maa.org/math-competitions/amc-1012] and AIME [https://www.maa.org/math-competitions/invitational-competitions] competitions, as well as two problems adapted from