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

OpenAI 表示，他们构建了一个用于 Lean 的神经定理证明器，学会解决多种具有挑战性的高中奥林匹克数学问题。题目包括 AMC12、AIME 的问题，以及两道由 IMO 题目改编的问题。