首页 > AI前沿 > Solving (some) formal math olympiad problems

Solving (some) formal math olympiad problems

OpenAI 2022-02-02 16:00 1 阅读 查看原文

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.