OpenAI、AIが生み出した数学の成果をLean証明付きで公開
Sharing AI Progress in Mathematics
OpenAIが内部のフロンティアモデルによって得られた数学の成果をGitHubで公開した。Institute for Advanced StudyのAdvisory Group on Mathematics and Artificial Intelligenceの助言に基づき、論文の改訂や引用のプロトコルを整備。多くの証明はLeanで形式化され、モデルの推論要約や計算コストの推定も含まれる。平均的な結果はChatGPT Proの約3時間分の計算に相当するという。
平均的な結果は、ChatGPT Proの思考およそ3時間分に相当する計算を使用した。