OpenAI News·· 2022-02-02AI 评分44
OpenAI 用 Lean 神经定理证明器求解部分国际数学奥林匹克难题
Solving (some) formal math olympiad problems
AI 导读
OpenAI 构建了一个面向 Lean 的神经定理证明器，学会了求解多道有挑战性的高中数学竞赛题，涵盖 AMC12、AIME 竞赛题目，以及两道改编自 IMO 的题目。
来源：OpenAI News · openai.com
OpenAI 用 Lean 神经定理证明器求解部分国际数学奥林匹克难题