OpenAI 构建 Lean 神经定理证明器，解出部分数学奥赛题

OpenAI 构建了一个面向 Lean 的神经定理证明器，能够解出多道高难度高中数学奥赛题，包括来自 AMC12 和 AIME 竞赛的题目，以及两道改编自 IMO 的题目。