OpenAI、数学の未解決問題で新成果 Lean証明も公開

OpenAIは、社内のフロンティアモデルを使って導いた、数学の未解決問題に関する新しい研究成果を公開しました。あわせてLeanによる証明の形式化と研究の詳細をGitHubで公開しており、数学者や開発者が内容を確認し、その上にさらに研究を積み上げられるようにしています。 これは、高度なAIシステムを数学的発見と検証の道具として位置づける、より大きな取り組みの一環です。形式証明支援ツールであるLeanを使うことで、OpenAIはモデルの推論を「もっともらしい」だけでなく検証可能なものにしようとしています。この違いは重要です。数学的主張は機械的に検証できるため、形式証明は、AIが本当に妥当な論証を見つけたのか、それとも尤もらしく見えるテキストを生成しただけなのかを、より厳しく試すことになります。証明とコードを公開することは外部の検証を招くことにもつながり、研究者が誤りや近道、明示されていない前提を見つける助けになり得ます。 この発表は熱狂と懸念の両方を呼び起こしました。支持する人は、広大な探索空間を調べ、予想を提示し、人間の直感の形式化を助ける強力な協働者としてAIを見ています。批判する人は、功績の帰属や信頼性、機械が未解決問題に貢献することの広い影響を心配しています。AIが新しい数学的知見を生み出すことが増えれば、成果をどう帰属させ、どう査読し、学術の慣行にどう組み込むかという問題が浮上します。フロンティアラボが数学研究の方向づけにおいて過大な役割を握るのではないか、という懸念もあります。 現時点では、OpenAIの公開はデモンストレーションであり、招待でもあると捉えるのが適切でしょう。AIが形式推論を加速し得ることを示す一方、丁寧な検証とコミュニティによる監督の必要性も浮き彫りにしています。数学者たちは証明を一行ずつ確かめる可能性が高く、その反応が、AIが数学的発見の日常的な一部になる速さを左右することになります。