Solving (some) formal math olympiad problems
OpenAI built a neural theorem prover for Lean that solved challenging high-school olympiad problems including AMC12, AIME, and adapted IMO problems.
Excerpt
We built a neural theorem prover for Lean that learned to solve a variety of challenging high-school olympiad problems, including problems from the AMC12 and AIME competitions, as well as two problems adapted from the IMO.
Read at source: https://openai.com/index/formal-math