OpenAI 研发 Lean 神经定理证明器并求解部分奥数题

OpenAI 构建了一个面向 Lean 的神经定理证明器，成功学会求解多种具有挑战性的高中数学奥赛题。该系统能够解答来自 AMC12 和 AIME 竞赛的题目，以及两道改编自国际数学奥林匹克（IMO）的试题。