OpenAI：官网动态·· 2022-02-02AI 评分52
OpenAI 构建神经定理证明器求解部分形式化数学奥赛题
Solving (some) formal math olympiad problems
AI 导读
OpenAI 构建了一个基于 Lean 的神经定理证明器，能求解多种有挑战性的高中奥赛题，包括 AMC12 和 AIME 竞赛题，以及两道由 IMO 改编的题目。
来源：OpenAI：官网动态 · openai.com
OpenAI 构建神经定理证明器求解部分形式化数学奥赛题