Solving (some) formal math olympiad problems
OpenAI Blog
A neural theorem prover was developed to solve challenging high-school mathematics olympiad problems in the Lean proof assistant. The system tackled problems from the AMC12 and AIME competitions, along with two adapted problems from the International Mathematical Olympiad. This demonstrates progress in using machine learning to handle formal mathematical reasoning at competition difficulty levels.
Why it matters
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.
