OpenAI 构建面向 Lean 的定理证明器，可求解部分奥数竞赛题

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